Editing Paradox (theorem prover)

{{Short description|Finite-domain model finder for pure first-order logic with equality}}
{{Infobox software
| name = Paradox
| logo = <!-- Image name is enough. -->
| logo alt = 
| logo caption = 
| screenshot = <!-- Image name is enough. -->
| screenshot alt = 
| caption = 
| collapsible = <!-- Any text here will collapse the screenshot. -->
| author = 
| developer = {{ubl|Koen Lindström Claessen|Niklas Sörensson}}
| released = <!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} -->
| discontinued = <!-- Set to yes if software is discontinued, otherwise omit. -->
| ver layout = <!-- simple (default) or stacked -->
| latest release version = 
| latest release date = <!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} -->
| latest preview version = 
| latest preview date = <!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} -->
| repo = <!-- {{URL|example.org}} -->
| programming language = [[Haskell]]
| operating system = 
| platform = 
| size = 
| language = 
| language count = <!-- Number only -->
| language footnote = 
| genre = [[Automated theorem proving]]
| license = [[GNU General Public License]]
| alexa = 
| website = <!-- {{URL|example.org}} -->
| standard = 
| AsOf = 
}}

'''Paradox''' is a finite-domain model finder for pure [[First-order logic#Equality and its axioms|first-order logic (FOL) with equality]] developed by Koen Lindström Claessen and Niklas Sörensson at the [[Chalmers University of Technology]].<ref name="Equinox-Paradox"/><ref name="Petr-P"/> It can a participate as part of an [[automated theorem proving]] system.<ref name="Petr-P"/> The software is primarily written in the [[Haskell programming language]].<ref name="CASC-6-Entrants"/> It is released under the terms of the [[GNU General Public License]] and is free.<ref name="Paradox-home-alone"/>

==Features==
The Paradox developers described the software as a ''[[Models And Counter-Examples|Mace]]-style'' method after the McCune's tool of that name.<ref name="Author-paper"/><ref name="Baumgartner-slides"/> The Paradox introduced new techniques which help to reduce the [[computational complexity]] of the [[Structure (mathematical logic)|model]] search problem:<ref name="Author-paper"/>
* ''term definitions'', new variable reduction technique,
* ''incremental satisfiability checker'' which works with small domains first, then gradually increases the size of the domain, reusing the information it obtained from previous failed searches,
* ''static symmetry reduction'' which adds extra constraints,
* ''sort inference'' which works with unsorted problems.

Paradox was developed up to version 4, the final version being effective in model finding for [[Web Ontology Language]] OWL2.<ref name="Hoot-too"/>

==Competition==
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.<ref name="CADE-comp-2018"/>

==References==
{{Reflist|refs=

<ref name="Petr-P">{{cite conference|conference=The 21st International Conference on Automated Deduction
|title=Semantic Selection of Premisses for Automated Theorem Proving|first=Petr|last=Pudlák
|book-title=Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories
|series=CEUR Workshop Proceedings|volume=257|pages=27–44|editor1=Urban, J. |editor2=Sutcliffe, G. |editor3=Schulz, S.
|location=Bremen|date=17 July 2007|s2cid=16318678 |issn=1613-0073
|url=https://pdfs.semanticscholar.org/d997/5c5ff3cb52393224fbe6a3fc78b4e4a54cba.pdf|access-date=7 November 2011|url-status=dead
|archive-url=https://web.archive.org/web/20181107222337/https://pdfs.semanticscholar.org/d997/5c5ff3cb52393224fbe6a3fc78b4e4a54cba.pdf
|archive-date=7 November 2018|df=dmy-all}}</ref>

<ref name="Hoot-too">{{cite arXiv|title=Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving
|first1=Michael|last1=Schneider|first2=Geoff|last2=Sutcliffe
|date=2011
|df=dmy-all|eprint=1108.0155|class=cs.AI}}</ref>

<ref name="CADE-comp-2018">{{cite web|url=http://tptp.cs.miami.edu/~tptp/CASC/|title=The CADE ATP System Competition - The World Championship for Automated Theorem Proving|id=Previous CASCs' Division Winners|access-date=7 November 2018
|url-status=live|archive-url=https://web.archive.org/web/20180901054747/http://tptp.cs.miami.edu/~tptp/CASC/|archive-date=1 September 2018|df=dmy-all}}</ref>

<ref name="CASC-6-Entrants">{{cite web|title=Entrants' System Descriptions|id=Paradox 3.0|website=University of Miami|access-date=7 November 2018
|url=http://tptp.cs.miami.edu/~tptp/CASC/J6/SystemDescriptions.html#Paradox---3.0
|archive-url=https://web.archive.org/web/20181107213954/http://tptp.cs.miami.edu/~tptp/CASC/J6/SystemDescriptions.html#Paradox---3.0|archive-date=7 November 2018|df=dmy-all}}</ref>

<ref name="Baumgartner-slides">{{cite web|title=Automated Theorem Proving|website=Australian National University College of Engineering & Computer Science|pages=73–74|url=http://users.cecs.anu.edu.au/~baumgart/teaching/logic-summer-school-2009-december/slides-automated-reasoning.pdf|access-date=11 November 2018|url-status=live|archive-url=https://web.archive.org/web/20181111205305/http://users.cecs.anu.edu.au/~baumgart/teaching/logic-summer-school-2009-december/slides-automated-reasoning.pdf|archive-date=11 November 2018|df=dmy-all}}</ref>

<!-- Primary and non independent -->

<!-- Alt reference that cant be waybacked: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.817.9812&rep=rep1&type=pdf -->
<ref name="Author-paper">{{Cite web|title=New Techniques that Improve MACE-style Finite Model Finding
|url=https://pdfs.semanticscholar.org/ca65/ae805d0fd210141d13a0f2d7be7a075bdd90.pdf
|access-date=11 November 2018
|first1=Koen|last1=Claessen|first2=Niklas|last2=Sörensson
|s2cid=15694927
|url-status=dead|archive-url=https://web.archive.org/web/20181111204329/https://pdfs.semanticscholar.org/ca65/ae805d0fd210141d13a0f2d7be7a075bdd90.pdf
|archive-date=11 November 2018|df=dmy-all}}</ref>

<ref name="Equinox-Paradox">{{cite web|url=http://www.cs.chalmers.se/~koen/folkung/|title=Paradox|website=[[Chalmers University of Technology]]|url-status=dead|archive-url=https://web.archive.org/web/20070108005818/http://www.cs.chalmers.se/~koen/folkung/|archive-date=8 January 2007|df=dmy-all|access-date=26 May 2007}}</ref>

<ref name="Paradox-home-alone">{{cite web|url=http://www.cs.chalmers.se:80/~koen/paradox/|title=Paradox|website=[[Chalmers University of Technology]]|url-status=dead|archive-url=https://web.archive.org/web/20070115083754/http://www.cs.chalmers.se/~koen/paradox/|archive-date=15 January 2007|df=dmy-all|access-date=30 April 2020}}</ref>
}}

{{Haskell programming}}

[[Category:Free theorem provers]]
[[Category:Free software programmed in Haskell]]
[[Category:Software using the GNU General Public License]]