Automatic Proof and Disproof in Isabelle/HOL
| Autor: | Lukas Bulwahn, Jasmin Christian Blanchette, Tobias Nipkow |
|---|---|
| Rok vydání: | 2011 |
| Předmět: |
Horn clause
Theoretical computer science business.industry Programming language Computer science Proof assistant HOL Resolution (logic) computer.software_genre Automation TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Compiler User interface business computer Counterexample |
| Zdroj: | Frontiers of Combining Systems ISBN: 9783642243639 FroCoS |
| DOI: | 10.1007/978-3-642-24364-6_2 |
| Popis: | Isabelle/HOL is a popular interactive theorem prover based on higherorder logic. It owes its success to its ease of use and powerful automation. Much of the automation is performed by external tools: The metaprover Sledgehammer relies on resolution provers and SMT solvers for its proof search, the counterexample generator Quickcheck uses the ML compiler as a fast evaluator for ground formulas, and its rival Nitpick is based on the model finder Kodkod, which performs a reduction to SAT. Together with the Isar structured proof format and a new asynchronous user interface, these tools have radically transformed the Isabelle user experience. This paper provides an overview of the main automatic proof and disproof tools. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|