Experiments on Supporting Interactive Proof Using Resolution
作者： Jia Meng , Lawrence C. Paulson
DOI: 10.1007/978-3-540-25984-8_28
关键词: Algorithm 、 Logical programming 、 Proof theory 、 Automated theorem proving 、 Resolution (logic) 、 Computer science 、 Conjunctive normal form 、 First-order logic 、 Programming language 、 Automated reasoning
摘要: Interactive theorem provers can model complex systems, but require much effort to prove theorems. Resolution are automatic and powerful, they designed be used for very different applications. This paper reports a series of experiments determine whether resolution support interactive proof as it is currently done. In particular, we present sound practical encoding in first-order logic Isabelle’s type classes.
springer.com
core.ac.uk
sci-hub.se 参考文章(26)
Alexandre Riazanov, Andrei Voronkov, Vampire 1.1 international joint conference on automated reasoning. pp. 376- 380 ,(2001) , 10.1007/3-540-45744-5_29
Peter F. Patel-Schneider, DLP System Description. Description Logics. ,(1998)
Thirty five years of automating mathematics Kluwer Academic Publishers. ,(2003) , 10.1007/978-94-017-0253-9
Alexandre Riazanov, Andrei Voronkov, Vampire 1.1 (System Description) international joint conference on automated reasoning. pp. 376- 380 ,(2001)
M. J. C. Gordon, T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic Cambridge University Press. ,(1993)
Christoph Weidenbach, Combining superposition, sorts and splitting Handbook of automated reasoning. pp. 1965- 2013 ,(2001) , 10.1016/B978-044450813-3/50029-1
Alexandre Riazanov, Andrei Voronkov, Efficient Checking of Term Ordering Constraints international joint conference on automated reasoning. pp. 60- 74 ,(2004) , 10.1007/978-3-540-25984-8_3
Richard Char-Tung Lee, Chin-Liang Chang, Symbolic Logic and Mechanical Theorem Proving ,(1973)
Andreas Nonnengart, Christoph Weidenbach, Computing small clause normal forms Handbook of Automated Reasoning. pp. 335- 367 ,(2001) , 10.1016/B978-044450813-3/50008-4
Andrei Voronkov, Alan Robinson, Handbook of automated reasoning Elsevier B.V.. ,(2001) , 10.1016/B978-044450813-3/50006-0