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.
[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.