swMATH ID: 3310
Software Authors: Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff
Description: 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.
Homepage: http://www.cs.miami.edu/~tptp/
Related Software: TPTP; E Theorem Prover; Isabelle/HOL; LEO-II; Satallax; TPS; HOL Light; Twelf; Metis_; HOL; SPASS; VAMPIRE; SystemOnTPTP; Leo; OMDoc; ILTP; Leo-III; Nitpick; MiniSat; Coq
Cited in: 14 Publications

Citations by Year