The Syntax

Annotated TPTP Formulae 

<language>(<name>,<user type>[-<source type>],
    <formula>[,
    <source>[,
    <useful info>]]).

Fields

  • <language> provides extensibility
  • <user type>[-<source type>] indicates semantics
    • User types: axiom, conjecture, lemma, ...
    • Source types: derived
  • <formula> uses TPTP FOF syntax
    • Follows user conventions
    • Compact, parsable, readable, writable, ASCII text
    • Same for CNF and FOF
    • Infix equality using = and !=
  • <source>
    • External: file, human, etc
    • Derived: inference term
  • <useful info> fields used for annotations, in same abstract syntax
          

Example FOF Problem Formula 

fof(extensionality,axiom,
    ! [X,Y] :
      ( X = Y
    <=> ( subclass(X,Y)
        & subclass(Y,X) ) ),
    file('SET005+0.ax',extensionality),
    [description('Principle of extensionality'),
     relevance(0.9)]).

Example CNF Derivation Formula 

cnf(140,lemma-derived,
    ( equal_sets(a,aUa)
    | member(member_of(a,aUa),a) ),
    inference(unit_del,[status(thm)],[
        inference(hyper,[status(thm)],[
            5,16]),11]),
    [iquote('hyper,5,16.1,unit_del,11')]).

Online