Developer(s) |
|
---|---|
Written in | Haskell |
Type | Automated theorem proving |
License | GNU General Public License |
Paradox is a finite-domain model finder for pure first-order logic (FOL) with equality developed by Koen Lindström Claessen and Niklas Sörensson at the Chalmers University of Technology. [1] [2] It can a participate as part of an automated theorem proving system. [2] The software is primarily written in the Haskell programming language. [3] It is released under the terms of the GNU General Public License and is free. [4]
The Paradox developers described the software as a Mace-style method after the McCune's tool of that name. [5] [6] The Paradox introduced new techniques which help to reduce the computational complexity of the model search problem: [5]
Paradox was developed up to version 4, the final version being effective in model finding for Web Ontology Language OWL2. [7]
Paradox was a division winner in the annual CADE ATP System Competition, an annual contest for automated theorem proving, in the years 2003 to 2012. [8]
Developer(s) |
|
---|---|
Written in | Haskell |
Type | Automated theorem proving |
License | GNU General Public License |
Paradox is a finite-domain model finder for pure first-order logic (FOL) with equality developed by Koen Lindström Claessen and Niklas Sörensson at the Chalmers University of Technology. [1] [2] It can a participate as part of an automated theorem proving system. [2] The software is primarily written in the Haskell programming language. [3] It is released under the terms of the GNU General Public License and is free. [4]
The Paradox developers described the software as a Mace-style method after the McCune's tool of that name. [5] [6] The Paradox introduced new techniques which help to reduce the computational complexity of the model search problem: [5]
Paradox was developed up to version 4, the final version being effective in model finding for Web Ontology Language OWL2. [7]
Paradox was a division winner in the annual CADE ATP System Competition, an annual contest for automated theorem proving, in the years 2003 to 2012. [8]