Automatic proof and disproof in Isabelle/HOL
作者： Jasmin Christian Blanchette , Lukas Bulwahn , Tobias Nipkow
DOI: 10.1007/978-3-642-24364-6_2
关键词:
摘要: Isabelle/HOL is a popular interactive theorem prover based on higherorder logic. It owes its success to ease of use and powerful automation. Much the automation performed by external tools: The metaprover Sledgehammer relies resolution provers SMT solvers for proof search, counterexample generator Quickcheck uses ML compiler as fast evaluator ground formulas, rival Nitpick model finder Kodkod, which performs reduction SAT. Together with Isar structured format new asynchronous user interface, these tools have radically transformed Isabelle experience. This paper provides an overview main automatic disproof tools.
springer.com
core.ac.uk
unsw.edu.au 
sci-hub.st 参考文章(69)
Kryštof Hoder, Andrei Voronkov, Sine Qua non for large theory reasoning conference on automated deduction. pp. 299- 314 ,(2011) , 10.1007/978-3-642-22438-6_23
Geoff Sutcliffe, System Description: SystemOn TPTP conference on automated deduction. pp. 406- 410 ,(2000)
Bruno Dutertre, Leonardo de Moura, The YICES SMT Solver ,(2006)
Geoff Sutcliffe, System Description: SystemOnTPTP conference on automated deduction. pp. 406- 410 ,(2000) , 10.1007/10721959_31
Koen Claessen, Ann Lillieström, Nicholas Smallbone, Sort it out with monotonicity: translating between many-sorted and unsorted first-order logic conference on automated deduction. pp. 207- 221 ,(2011) , 10.1007/978-3-642-22438-6_17
James A. Storer, Induction and Recursion Birkhäuser, Boston, MA. pp. 87- 125 ,(2002) , 10.1007/978-1-4612-0075-8_3
Stephan Schulz, Jürgen Zimmer, Geoff Sutcliffe, TSTP Data-Exchange Formats for Automated Theorem Proving Tools ,(2004)
Ben diVito, Myla Archer, Cesar Munoz, Design and Application of Strategies/Tactics in Higher Order Logics ,(2003)
Fredrik Lindblad, Property Directed Generation of First-Order Test Data trends in functional programming. ,vol. 8, pp. 105- 123 ,(2008)
Lawrence C. Paulson, Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers PAAR@IJCAR. pp. 1- 10 ,(2010)