Paradox (theorem prover)
From Wikipedia, the free encyclopedia
| Paradox | |
|---|---|
| Original author(s) |
|
| Developer(s) | Chalmers University of Technology |
| Initial release | 2003 |
| Final release | 4
/ 2011 |
| Written in | Haskell |
| Available in | English |
| 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 written mostly in the programming language Haskell.[3] It is free and open-source software released under the terms of the GNU General Public License.[4]
