Concrete Syntax

Annotated Formulae

• language(name, role, formula, source, useful info).

• language provides extensibility ... cnf, fof, tff, thf
• role indicates user semantics, e.g.,
  • For problems: axiom, conjecture, lemma, ...
  • For solutions: axiom, plain, assumption, ...
• formula uses TPTP syntax
  • Prolog-like (no Greek letters, only Roman)
  • Connectives ... !, ?, ~, |, &, =>, <=, <=>, <~>.
  • Easily identified Interpreted symbols
  • Equality ... =, !=
  • Easy to parse (esp. in Prolog :-)
• source
  • External: file, human, etc
  • Derived: inference term
• useful info fields used for annotations, in same abstract syntax

Example FOF Problem Formula

fof(subclass_defn,axiom,
    ! [X,Y] : 
      ( subclass(X,Y)
    <=> ! [U] : 
          ( member(U,X)
         => member(U,Y) ) ),
    file('SET005+0.ax',subclass_defn),
    [description('Definition of subclass'),
     relevance(0.9)]).
          

Example CNF Solution Formula

cnf(140,lemma,
    ( 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')]).