Abstract Syntax

Annotated TSTP Formulae

<language>(<name>,<role>,
    <formula>[,
    <source>[,
    <useful info>]]).
          

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,derived-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')]).