THF0

THF0 is a syntactically conservative extension of the untyped first-order TPTP language, adding the syntax for higher-order logic. Maintaining a consistent style between the first-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 definitions. There are good reasons for maintaining Prolog compatibility.


References in zbMATH (referenced in 14 articles , 1 standard article )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
  2. Libal, Tomer; Miller, Dale: Functions-as-constructors higher-order unification (2016)
  3. Benzmüller, Christoph: Higher-order automated theorem provers (2015)
  4. Horozal, Fulya; Rabe, Florian: Formal logic definitions for interchange languages (2015)
  5. Sultana, Nik; Benzmüller, Christoph; Paulson, Lawrence C.: Proofs and reconstructions (2015)
  6. Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Baumgartner, Peter: The TPTP typed first-order form with arithmetic (2012)
  7. Benzmüller, Christoph: Combining and automating classical and non-classical logics in classical higher-order logics (2011)
  8. Benzmüller, Christoph: Verifying the modal logic cube is an easy task (for higher-order automated reasoners) (2010)
  9. Benzmüller, Christoph: Combining logics in simple type theory (2010)
  10. Sutcliffe, Geoff: The TPTP World -- infrastructure for automated reasoning (2010)
  11. Sutcliffe, Geoff; Benzmüller, Christoph: Automated reasoning in higher-order logic using the TPTP THF infrastructure (2010)
  12. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
  13. Sutcliffe, Geoff; Benzmüller, Christoph; Brown, Chad E.; Theiss, Frank: Progress in the development of automated theorem proving for higher-order logic (2009)
  14. Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff: THF0 -- the core of the TPTP language for higher-order logic (2008)