×

THF0 – the core of the TPTP language for higher-order logic. (English) Zbl 1165.68447

Armando, Alessandro (ed.) et al., Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008 Proceedings. Berlin: Springer (ISBN 978-3-540-71069-1/pbk). Lecture Notes in Computer Science 5195. Lecture Notes in Artificial Intelligence, 491-506 (2008).
Summary: One of the keys to the success of the Thousands of Problems for Theorem Provers (TPTP) problem library and related infrastructure is the consistent use of the TPTP language. This paper introduces the core of the TPTP language for higher-order logic – THF0, based on Church’s simple type theory. THF0 is a syntactically conservative extension of the untyped first-order TPTP language.
For the entire collection see [Zbl 1149.68003].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

TPTP; HOL Light; THF0; TPS
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Andrews, P. B.; Bishop, M.; Issar, S.; Nesmith, D.; Pfenning, F.; Xi, H., TPS: A Theorem-Proving System for Classical Type Theory, Journal of Automated Reasoning, 16, 3, 321-353 (1996) · Zbl 0858.03017 · doi:10.1007/BF00252180
[2] Beeson, M.: Otter-lambda, a Theorem-prover with Untyped Lambda-unification. In: Sutcliffe, G., Schulz, S., Tammet, T. (eds.) Proceedings of the Workshop on Empirically Successful First Order Reasoning (2004)
[3] Benzmüller, C.; Brown, C.; Hurd, J.; Melham, T., A Structured Set of Higher-Order Problems, Theorem Proving in Higher Order Logics, 66-81 (2005), Heidelberg: Springer, Heidelberg · Zbl 1152.68517
[4] Benzmüller, C.; Brown, C.; Kohlhase, M., Higher-order Semantics and Extensionality, Journal of Symbolic Logic, 69, 4, 1027-1088 (2004) · Zbl 1071.03024 · doi:10.2178/jsl/1102022211
[5] Benzmüller, C.; Kohlhase, M.; Kirchner, C.; Kirchner, H., LEO - A Higher-Order Theorem Prover, Automated Deduction - CADE-15, 139-143 (1998), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0054256
[6] Benzmüller, C., Paulson, L.: Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. In: Benzmüller, C., Brown, C., Siekmann, J., Statman, R. (eds.) Festschrift in Honour of Peter B. Andrews on his 70th Birthday. IfCoLog (to appear 2007) · Zbl 1227.03017
[7] Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined Reasoning by Automated Cooperation. Journal of Applied Logic (in print) (2008) · Zbl 1162.68646
[8] Benzmüller, C.; Theiss, F.; Paulson, L.; Fietzke, A.; Armando, A.; Baumgartner, P.; Dowek, G., LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic, Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008) (2008), Heidelberg: Springer, Heidelberg · Zbl 1165.68446
[9] Church, A., A Formulation of the Simple Theory of Types, Journal of Symbolic Logic, 5, 56-68 (1940) · Zbl 0023.28901 · doi:10.2307/2266170
[10] Curry, H. B.; Feys, R., Combinatory Logic I (1958), Amsterdam: North Holland, Amsterdam · Zbl 0081.24104
[11] Frege, F.: Grundgesetze der Arithmetik. Jena (1893) (1903) · JFM 34.0071.05
[12] Godefroid, P.: Software Model Checking: the VeriSoft Approach. Technical Report Technical Memorandum ITD-03-44189G, Bell Labs, Lisle, USA (2003)
[13] Gordon, M.; Melham, T., Introduction to HOL, a Theorem Proving Environment for Higher Order Logic (1993), Cambridge: Cambridge University Press, Cambridge · Zbl 0779.68007
[14] Harper, R.; Honsell, F.; Plotkin, G., A Framework for Defining Logics, Journal of the ACM, 40, 1, 143-184 (1993) · Zbl 0778.03004 · doi:10.1145/138027.138060
[15] Harrison, J.; Srivas, M.; Camilleri, A., HOL Light: A Tutorial Introduction, Formal Methods in Computer-Aided Design, 265-269 (1996), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0031814
[16] Henkin, L., Completeness in the Theory of Types, Journal of Symbolic Logic, 15, 81-91 (1950) · Zbl 0039.00801 · doi:10.2307/2266967
[17] Howard, W.; Seldin, J.; Hindley, J., The Formulas-as-types Notion of Construction, H B Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism, 479-490 (1980), London: Academic Press, London · Zbl 0469.03006
[18] Martin-Löf, P.; Sambin, G.; Smith, J., An Intuitionistic Theory of Types, Twenty-Five Years of Constructive Type Theory, 127-172 (1973), Oxford: Oxford University Press, Oxford · Zbl 0931.03070
[19] Matuszek, C., Cabral, J., Witbrock, M., DeOliveira, J.: An Introduction to the Syntax and Content of Cyc. In: Baral, C. (ed.) Proceedings of the 2006 AAAI Spring Symposium on Formalizing and Compiling Background Knowledge and Its Applications to Knowledge Representation and Question Answering, pp. 44-49 (2006)
[20] Niles, I., Pease, A.: Towards A Standard Upper Ontology. In: Welty, C., Smith, B. (eds.) Proceedings of the 2nd International Conference on Formal Ontology in Information Systems, pp. 2-9 (2001)
[21] Nipkow, T.; Paulson, L. C.; Wenzel, M. T., Isabelle/HOL (2002), Heidelberg: Springer, Heidelberg · Zbl 0994.68131
[22] Owre, S.; Rajan, S.; Rushby, J. M.; Shankar, N.; Srivas, M.; Alur, R.; Henzinger, T. A., PVS: Combining Specification, Proof Checking, and Model Checking, Computer Aided Verification, 411-414 (1996), Heidelberg: Springer, Heidelberg
[23] Pfenning, F.; Schürmann, C.; Ganzinger, H., System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Automated Deduction - CADE-16, 202-206 (1999), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-48660-7_14
[24] Rudnicki, P.: An Overview of the Mizar Project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311-332 (1992)
[25] Siekmann, J.; Benzmüller, C.; Autexier, S., Computer supported mathematics with omega, Journal of Applied Logic, 4, 4, 533-559 (2006) · Zbl 1107.68101 · doi:10.1016/j.jal.2005.10.008
[26] Sutcliffe, G.; Diekert, V.; Volkov, M. V.; Voronkov, A., TPTP, TSTP, CASC, etc, Computer Science - Theory and Applications, 7-23 (2007), Heidelberg: Springer, Heidelberg · Zbl 1188.68265 · doi:10.1007/978-3-540-74510-5_4
[27] Sutcliffe, G.; Schulz, S.; Claessen, K.; Gelder, A. V.; Furbach, U.; Shankar, N., Using the TPTP Language for Writing Derivations and Finite Interpretations, Automated Reasoning, 67-81 (2006), Heidelberg: Springer, Heidelberg · Zbl 1222.68373 · doi:10.1007/11814771_7
[28] Sutcliffe, G.; Suttner, C., The State of CASC, AI Communications, 19, 1, 35-48 (2006) · Zbl 1112.68464
[29] Sutcliffe, G.; Suttner, C. B., The TPTP Problem Library: CNF Release v1.2.1, Journal of Automated Reasoning, 21, 2, 177-203 (1998) · Zbl 0910.68197 · doi:10.1023/A:1005806324129
[30] Sutcliffe, G.; Zimmer, J.; Schulz, S.; Zhang, W.; Sorge, V., TSTP Data-Exchange Formats for Automated Theorem Proving Tools, Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, 201-215 (2004), Amsterdam: IOS Press, Amsterdam · Zbl 1069.68098
[31] Gelder, A. V.; Sutcliffe, G.; Furbach, U.; Shankar, N., Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation, Automated Reasoning, 156-161 (2006), Heidelberg: Springer, Heidelberg · Zbl 1222.68375 · doi:10.1007/11814771_15
[32] Zermelo, E., Über Grenzzahlen und Mengenbereiche, Fundamenta Mathematicae, 16, 29-47 (1930) · JFM 56.0082.02
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.