The top level building blocks of TPTP derivation files are annotated formulae and comments. An annotated formula has the form:
language(name,role,formula,source,useful info).
The useful information is optional. The languages currently supported are thf - typed higher-order form, tff - typed first-order form, fof - (full) first-order form, and cnf - clause normal form.
A derivation is a list of annotated formulae, typically without the useful information. (This is a description of an ordinary derivation - the TPTP language can do a lot more than this.)
Name: The name is a word starting lower case, e.g., original_f1, or a single quoted word, e.g., 'A crazy $ name'.
Role: The role is typically one of axiom for axiom leaves, definition for definition leaves, conjecture for conjecture leaves, negated_conjecture for negated conjectures, or plain for inferred formulae. A full list of the possible roles is in the TPTP syntax.
Logical formula: The logical formula uses the TPTP syntax for formulae.
Source: Each leaf formula has a file() record or an introduced() record, and each inferred formula has an inference() record. Details below.
The annotated formulae define the leaves and inferred formulae of the derivation. All the details are in the documentation for the TPTP language.
File records
A file() record contains the problem file name and the corresponding annotated formula name in the problem file, e.g.:
fof(john,axiom,
human(john),
file('CreatedEqual.p',john) ).
Introduced records
An introduced() record contains the introduction rule name, a list of useful introduction information, and a list of any parent formulae, e.g.:
fof(64,definition,
( sP1 <=> ! [X8] : ~ has_job(X8,boxer) ),
introduced(definition,[new_symbols(definition,[sP1])],[])).
The introduction() records for definitions that introduce new symbol, for introduced tautologies, and theory axioms that have to be accepted on faith, e.g., arithmetic axioms, have particular requirements.
Inference records
An inference() record contains the inference rule name, a list of useful inference information, and a list of its parents. Parents are annotated formula names or nested inference() records. Example:
cnf(c_0_20,negated_conjecture,
sK0 = john,
inference(cn,[status(thm)],[c_0_15,inference(rw,[status(thm)],[c_0_16,c_0_17])]) ).
Common types of useful inference information are:
The semantic relationship of the formula to its parents as an SZS ontology value in a status() record. The most common ones are status(thm) when the inferred formula is a theorem (logical consequence) of its parents, status(cth) when the negation of the inferred formula is a theorem (logical consequence) of its parents, e.g., the step negating the conjecture for a proof by refutation, and status(esa) when the inferred formula is equisatisfiable with its single parent, e.g., Skolemization steps.
Special information about recognized types of inferences, e.g., Skolemization.
Details of new symbols introduced in the inference, e.g., by Herbrandization, documented in a new_symbols() record. New symbols should follow the conventions for new symbol names.
Here is a CNF refutation for the toy problem in the Problems page:
%------------------------------------------------------------------------
fof(all_created_equal,axiom,
! [H1,H2] :
( ( human(H1)
& human(H2) )
=> created_equal(H1,H2) ),
file('EqualHumans.p',all_created_equal) ).
fof(someone_got_an_a,axiom,
? [H] :
( human(H)
& grade(H) = a ),
file('EqualHumans.p',someone_got_an_a) ).
fof(someone_not_john,conjecture,
? [H] :
( human(H)
& created_equal(H,john)
& H != john ),
file('EqualHumans.p',someone_not_john) ).
fof(someone_not_john_neg,negated_conjecture,
~ ? [H] :
( human(H)
& created_equal(H,john)
& H != john ),
inference(assume_negation,[status(cth)],[someone_not_john]) ).
cnf(c_5,plain,
( ~ human(A)
| ~ human(B)
| created_equal(A,B) ),
inference(clausify,[status(thm)],[all_created_equal]) ).
fof(john,axiom,
human(john),
file('EqualHumans.p',john) ).
cnf(c_6,plain,
human(john),
inference(clausify,[status(thm)],[john]) ).
fof(john_failed,axiom,
grade(john) = f,
file('EqualHumans.p',john_failed) ).
cnf(c_7,plain,
grade(john) = f,
inference(clausify,[status(thm)],[john_failed]) ).
cnf(c_8,plain,
f = grade(john),
inference(copy,[status(thm)],[c_7]) ).
fof(nnf_2,plain,
? [H] :
( human(H)
& grade(H) = a ),
inference(fof_nnf,[status(thm)],[someone_got_an_a]) ).
fof(sk_someone_got_an_a,plain,
( human(sK0)
& grade(sK0) = a ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(H,sK0)],[nnf_2]) ).
cnf(c_9,plain,
human(sK0),
inference(split_conjunct,[status(thm)],[sk_someone_got_an_a]) ).
cnf(c_10,plain,
grade(sK0) = a,
inference(split_conjunct,[status(thm)],[sk_someone_got_an_a]) ).
cnf(c_11,plain,
a = grade(sK0),
inference(copy,[status(thm)],[c_10]) ).
fof(distinct_grades,axiom,
a != f,
file('EqualHumans.p',distinct_grades) ).
cnf(c_12,plain,
a != f,
inference(clausify,[status(thm)],[distinct_grades]) ).
cnf(c_23,plain,
grade(sK0) != f,
inference(paramod,[status(thm)],[c_11,c_12]) ).
cnf(c_13,plain,
grade(sK0) != grade(john),
inference(paramod,[status(thm)],[c_8,c_23]) ).
cnf(c_15,negated_conjecture,
( ~ human(A)
| ~ created_equal(A,john)
| A = john ),
inference(clausify,[status(thm)],[someone_not_john_neg]) ).
cnf(c_16,negated_conjecture,
( ~ human(A)
| ~ created_equal(A,john)
| john = A ),
inference(copy,[status(thm)],[c_15]) ).
cnf(c_24,plain,
( ~ human(A)
| created_equal(sK0,A) ),
inference(resolve,[status(thm)],[c_5,c_9]) ).
cnf(c_20,plain,
created_equal(sK0,john),
inference(resolve,[status(thm)],[c_24,c_6]) ).
cnf(c_25,negated_conjecture,
( ~ created_equal(sK0,john)
| john = sK0 ),
inference(resolve,[status(thm)],[c_16,c_9]) ).
cnf(c_26,negated_conjecture,
john = sK0,
inference(resolve,[status(thm)],[c_25,c_20]) ).
cnf(c_21,negated_conjecture,
sK0 = john,
inference(copy,[status(thm)],[c_26]) ).
cnf(c_27,plain,
grade(john) != grade(john),
inference(paramod,[status(thm)],[c_21,c_13]) ).
cnf(c_22,plain,
$false,
inference(copy,[status(thm)],[c_27]) ).
%------------------------------------------------------------------------
A quick way to check the syntax of a derivation is to run it through tptp4X, available online in SystemOnTSTP. Select the "Input formulae" option and paste the formulae into the text box. Select tptp4X as the system (or select no System - TPTP4X is the default). ProcessProblem, and if the syntax is faulty an error massage will be returned.
Once the syntax is OK, choose the GDV derivation verifier system. RunSelectedSystems and see if it verifies the derivation. For more information about GDV read ...
@Article{Sut06,
Author = "Sutcliffe, G.",
Year = "2006",
Title = "{Semantic Derivation Verification}",
Journal = "International Journal on Artificial Intelligence Tools",
Volume = "15",
Number = "6",
Pages = "1053-1070"
}