Annotated TSTP Formulae
<language>(<name>,<role>,
<formula>[,
<source>[,
<useful info>]]).
Fields
- <language> provides extensibility
- <role> indicates user semantics, e.g.,
- For problems: axiom, conjecture,
lemma, ...
- For solutions: axiom, plain,
assumption, ...
- <formula> uses TPTP syntax
- Follows user conventions
- Compact ASCII text
- 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')]).
|