TPTP; Automated reasoning; First order logic; Interpretation; Model finding; Computer Science (all)
Abstract :
[en] This paper describes a new format for representing Tarskian-style interpretations for formulae in typed first-order logic, using the TPTP TF0 language. It further describes a technique and an implemented tool for verifying models using this representation, and a tool for visualizing interpretations. The research contributes to the advancement of automated reasoning technology for model finding, which has several applications, including verification.
Disciplines :
Computer science
Author, co-author :
Steen, Alexander; University of Greifswald, Greifswald, Germany
Sutcliffe, Geoff; University of Miami, Miami, United States
Fontaine, Pascal ; Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore) > Systèmes informatiques distribués
McKeown, Jack; University of Miami, Miami, United States
Language :
English
Title :
Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
Publication date :
2023
Event name :
Logic for Programming, Artificial Intelligence and Reasoning
C. Alrabbaa, F. Baader, S. Borgwardt, R. Dachselt, P. Koopmann, and J. Mendez. Evonne: Interactive Proof Visualization for Description Logics (System Description). In J. Blanchette, L. Kovacs, and D. Pattinson, editors, Proceedings of the 11th International Joint Conference on Automated Reasoning, number 13385 in Lecture Notes in Artificial Intelligence, pages 271-280, 2022
A.R. Anderson and N.D. Belnap. Entailment: The Logic of Relevance and Necessity, Vol. 1. Princton University Press, 1975
L. Augusto. Many-valued Logics: A Mathematical and Computational Introduction. College Publications, 2017
D. Babic. Satisfiability Suggested Format. https://www.domagoj-babic.com/uploads/ ResearchProjects/Spear/dimacs-cnf.pdf, 1993
L. Bachmair, H. Ganzinger, D. McAllester, and C. Lynch. Resolution Theorem Proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pages 19-99. Elsevier Science, 2001
C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB Standard: Version 2.6. https://smtlib.cs.uiowa.edu, 2017
C. Battel. Treehehe: An interactive visualization of proof trees. https://github.com/seachel/treehehe, 2018
P. Blackburn, J. van Benthem, and F. Wolther. Handbook of Modal Logic. Number 3 in Studies in Logic and Practical Reasoning. Elsevier Science, 2006
J. Blanchette and T. Nipkow. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In M. Kaufmann and L. Paulson, editors, Proceedings of the 1st International Conference on Interactive Theorem Proving, number 6172 in Lecture Notes in Computer Science, pages 131-146. Springer-Verlag, 2010
J. Blanchette and A. Paskevich. TFF1: The TPTP Typed First-order Form with Rank-1 Polymorphism. In M.P. Bonacina, editor, Proceedings of the 24th International Conference on Automated Deduction, number 7898 in Lecture Notes in Artificial Intelligence, pages 414-420. Springer-Verlag, 2013
K. Claessen and N. So¨rensson. New Techniques that Improve MACE-style Finite Model Finding. In P. Baumgartner and C. Fermueller, editors, Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications, 2003
A.G. Cohn. A More Expressive Formulation of Many Sorted Logic. Journal of Automated Reasoning, 3(2):113-200, 1987
L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In C. Ramakrishnan and J. Rehof, editors, Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, number 4963 in Lecture Notes in Artificial Intelligence, pages 337-340. Springer-Verlag, 2008
V. D’Silva, D. Kroening, and G. Weissenbacher. A Survey of Automated Techniques for Formal Software Verification. IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems, 27(7):1165-1178, 2008
J. Ellson, E. Gansner, L. Koutsofios, S. North, and G. Woodhull. Graphviz - Open Source Graph Drawing Tools. In P. Mutzel, M. Ju¨nger, and S. Leipert, editors, Proceedings of the 9th International Symposium on Graph Drawing, number 2265 in Lecture Notes in Computer Science, pages 483-484. Springer-Verlag, 2002
J. Gallier. Logic for Computer Science - Foundations of Automatic Theorem Proving. Dover Publications, 2015
J. Herbrand. Recherches sur la Theorie de la Demonstration. Travaux de la Societe des Sciences et des Lettres de Varsovie, Class III, Sciences Mathematiques et Physiques, 33, 1930
F. Horozal and F. Rabe. Formal Logic Definitions for Interchange Languages. In M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge, editors, Proceedings of the International Conference on Intelligent Computer Mathematics, number 9150 in Lecture Notes in Computer Science, pages 171-186. Springer-Verlag, 2015
G. Hunter. Metalogic: An Introduction to the Metatheory of Standard First Order Logic. University of California Press, 1996
M. Ja¨rvisalo, D. Le Berre, O. Roussel, and L. Simon. The International SAT Solver Competitions. AI Magazine, 33(1):89-92, 2012
C. Kaliszyk, G. Sutcliffe, and F. Rabe. TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. In P. Fontaine, S. Schulz, and J. Urban, editors, Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning, number 1635 in CEUR Workshop Proceedings, pages 41-55, 2016
L. Kovacs and A. Voronkov. First-Order Theorem Proving and Vampire. In N. Sharygina and H. Veith, editors, Proceedings of the 25th International Conference on Computer Aided Verification, number 8044 in Lecture Notes in Artificial Intelligence, pages 1-35. Springer-Verlag, 2013
S. Kripke. Semantical Considerations on Modal Logic. Acta Philosophica Fennica, 16:83-94, 1963
W.W. McCune. Mace4 Reference Manual and Guide. Technical Report ANL/MCS-TM-264, Argonne National Laboratory, Argonne, USA, 2003
W.W. McCune. Otter 3.3 Reference Manual. Technical Report ANL/MSC-TM-263, Argonne National Laboratory, Argonne, USA, 2003
G. Priest. Paraconsistent Logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 6, pages 287-393. Springer-Verlag, 2002
A. Robinson and A. Voronkov. Handbook of Automated Reasoning. Elsevier Science, 2001
C. Schlyter. Visualization of a Finite First Order Logic Model. Master’s thesis, Department of Computer Science and Engineering, University of Gothenburg, Go¨teborg, Sweden, 2013
M. Schmidt-Schauss. A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. In Joshi A., editor, Proceedings of the 9th International Joint Conference on Artificial Intelligence, pages 1162-1168. IJCAI Organization, 1985
S. Schulz, S. Cruanes, and P. Vukmirovic. Faster, Higher, Stronger: E 2.3. In P. Fontaine, editor, Proceedings of the 27th International Conference on Automated Deduction, number 11716 in Lecture Notes in Computer Science, pages 495-507. Springer-Verlag, 2019
S. Schulz, G. Sutcliffe, J. Urban, and A. Pease. Detecting Inconsistencies in Large First-Order Knowledge Bases. In L. de Moura, editor, Proceedings of the 26th International Conference on Automated Deduction, number 10395 in Lecture Notes in Computer Science, pages 310-325. SpringerVerlag, 2017
A. Steen, D. Fuenmayor, T. Gleißner, G. Sutcliffe, and C. Benzmu¨ller. Automated Reasoning in Non-classical Logics in the TPTP World. In B. Konev, C. Schon, and A. Steen, editors, Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning, number 3201 in CEUR Workshop Proceedings, page Online, 2022
G. Sutcliffe. Semantic Derivation Verification: Techniques and Implementation. International Journal on Artificial Intelligence Tools, 15(6):1053-1070, 2006
G. Sutcliffe. TPTP, TSTP, CASC, etc. In V. Diekert, M. Volkov, and A. Voronkov, editors, Proceedings of the 2nd International Symposium on Computer Science in Russia, number 4649 in Lecture Notes in Computer Science, pages 6-22. Springer-Verlag, 2007
G. Sutcliffe. The SZS Ontologies for Automated Reasoning Software. In G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz, editors, Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, number 418 in CEUR Workshop Proceedings, pages 38-49, 2008
G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning, 43(4):337-362, 2009
G. Sutcliffe. The TPTP World - Infrastructure for Automated Reasoning. In E. Clarke and A. Voronkov, editors, Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, number 6355 in Lecture Notes in Artificial Intelligence, pages 1-12. Springer-Verlag, 2010
G. Sutcliffe. The CADE ATP System Competition - CASC. AI Magazine, 37(2):99-101, 2016
G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483-502, 2017
G. Sutcliffe. The Logic Languages of the TPTP World. Logic Journal of the IGPL, page https://doi.org/10.1093/jigpal/jzac068, 2022
G. Sutcliffe and C. Benzmu¨ller. Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of Formalized Reasoning, 3(1):1-27, 2010
G. Sutcliffe and E. Kotelnikov. TFX: The TPTP Extended Typed First-order Form. In B. Konev, J. Urban, and S. Schulz, editors, Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning, number 2162 in CEUR Workshop Proceedings, pages 72-87, 2018
G. Sutcliffe, S. Schulz, K. Claessen, and P. Baumgartner. The TPTP Typed First-order Form with Arithmetic. In N. Bjørner and A. Voronkov, editors, Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, number 7180 in Lecture Notes in Artificial Intelligence, pages 406-419. Springer-Verlag, 2012
G. Sutcliffe, S. Schulz, K. Claessen, and A. Van Gelder. Using the TPTP Language for Writing Derivations and Finite Interpretations. In U. Furbach and N. Shankar, editors, Proceedings of the 3rd International Joint Conference on Automated Reasoning, number 4130 in Lecture Notes in Artificial Intelligence, pages 67-81. Springer, 2006
G. Sutcliffe and C.B. Suttner. The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning, 21(2):177-203, 1998
A. Tarski and R. Vaught. Arithmetical Extensions of Relational Systems. Compositio Mathematica, 13:81-102, 1956
H. Tews. Proof tree visualization for proof general. http://askra.de/software/prooftree/, 2017
S. Trac, Y. Puzis, and G. Sutcliffe. An Interactive Derivation Viewer. In S. Autexier and C. Benzmu¨ller, editors, Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, volume 174 of Electronic Notes in Theoretical Computer Science, pages 109-123, 2007
A. Van Gelder and G. Sutcliffe. Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. In U. Furbach and N. Shankar, editors, Proceedings of the 3rd International Joint Conference on Automated Reasoning, number 4130 in Lecture Notes in Artificial Intelligence, pages 156-161. Springer-Verlag, 2006
P. Vukmirovic, A. Bentkamp, J. Blanchette, S. Cruanes, V. Nummelin, and S. Tourret. Making Higher-order Superposition Work. In A. Platzer and G. Sutcliffe, editors, Proceedings of the 28th International Conference on Automated Deduction, number 12699 in Lecture Notes in Computer Science, pages 415-432. Springer-Verlag, 2021
C. Walther. A Many-Sorted Calculus Based on Resolution and Paramodulation. In Bundy A., editor, Proceedings of the 8th International Joint Conference on Artificial Intelligence, pages 882- 891, 1983
S. Winker. Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions. Journal of the ACM, 29(2):273-284, 1982
