| 词条 | Paradox (theorem prover) |
| 释义 |
| name = Paradox | logo = | logo alt = | logo caption = | screenshot = | screenshot alt = | caption = | collapsible = | author = | developer = {{ubl|Koen Lindström Claessen|Niklas Sörensson}} | released = | discontinued = | ver layout = | latest release version = | latest release date = | latest preview version = | latest preview date = | repo = | programming language = | operating system = | platform = | size = | language = | language count = | language footnote = | genre = automated theorem proving | license = | alexa = | website = | standard = | AsOf = }}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] It can a participate as part of an automated theorem proving system.{{cn|date=November 2018}} 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] FeaturesThe Paradox developers described the software as a Mace-style method after the McCune's tool of that name.[5][6] Paradox was developed up to version 4, the final version being effective in model finding for Web Ontology Language OWL2.[7] CompetitionParadox 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] References1. ^1 {{cite web|title=Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving|first1=Michael|last1=Schneider|first2=Geoff|last2=Sutcliffe||url=https://arxiv.org/pdf/1108.0155.pdf|access-date=11 November 2018|date=2011|dead-url=no|archive-url=https://web.archive.org/web/20181111205826/https://arxiv.org/pdf/1108.0155.pdf|archive-date=18 November 2018|df=dmy-all}} [1][2][3][4][5][6][7]2. ^1 {{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|dead-url=no|archive-url=https://web.archive.org/web/20180901054747/http://tptp.cs.miami.edu/~tptp/CASC/|archive-date=1 September 2018|df=dmy-all}} 3. ^1 {{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}} 4. ^1 {{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||dead-url=no|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}} 5. ^1 {{Cite web|title=New Techniques that Improve MACE-style Finite Model Finding|url=https://pdfs.semanticscholar.org/ca65/ae805d0fd210141d13a0f2d7be7a075bdd90.pdf?_ga=2.240348995.1727082969.1541961710-1050754363.1531062097|access-date=11 November 2018|first1=Koen|last1=Claessen|first2=Niklas|last2=Sörensson|dead-url=no|archive-url=https://web.archive.org/web/20181111184344/https://pdfs.semanticscholar.org/ca65/ae805d0fd210141d13a0f2d7be7a075bdd90.pdf?_ga=2.240348995.1727082969.1541961710-1050754363.1531062097|archive-date=11 November 2018|df=dmy-all}} 6. ^1 {{cite web|url=http://www.cs.chalmers.se/~koen/folkung/|title=Paradox|website=Chalmers University of Technology|dead-url=yes|archive-url=https://web.archive.org/20070108005818/http://www.cs.chalmers.se/~koen/folkung/|archive-date=8 January 2007|df=dmy-all}} 7. ^1 {{cite web|url=http://www.cs.chalmers.se:80/~koen/paradox/|title=Paradox|website=Chalmers University of Technology|dead-url=yes|archive-url=https://web.archive.org/web/20070115083754/http://www.cs.chalmers.se:80/~koen/paradox/|archive-date=15 January 2007|df=dmy-all}} }}{{compu-sci-stub}}{{free-software-stub}} 2 : Free theorem provers|Free software programmed in Haskell |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。