THF0 is a syntactically conservative extension of the untyped ﬁrst-order TPTP language, adding the syntax for higher-order logic. Maintaining a consistent style between the ﬁrst-order and higher-order languages facilitates easy adoption of the new language, through reuse or adaptation of existing infrastructure for processing TPTP format data, e.g., parsing tools, pretty-printing tools, system testing, and result analysis, (see Section 5). A particular feature of the TPTP language, which has been maintained in THF0, is Prolog compatibility. This allows an annotated formula to be read with a single Prolog read/1 call, in the context of appropriate operator deﬁnitions. There are good reasons for maintaining Prolog compatibility.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Baumgartner, Peter: The TPTP typed first-order form with arithmetic (2012)
- Benzmüller, Christoph: Combining and automating classical and non-classical logics in classical higher-order logics (2011)
- Benzmüller, Christoph: Combining logics in simple type theory (2010)
- Benzmüller, Christoph: Verifying the modal logic cube is an easy task (for higher-order automated reasoners) (2010)
- Sutcliffe, Geoff; Benzmüller, Christoph: Automated reasoning in higher-order logic using the TPTP THF infrastructure (2010)
- Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
- Sutcliffe, Geoff; Benzmüller, Christoph; Brown, Chad E.; Theiss, Frank: Progress in the development of automated theorem proving for higher-order logic (2009)
- Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff: THF0 -- the core of the TPTP language for higher-order logic (2008)