public class THF
This class handles the conversion of problems (= axioms + queries)
from their KIF representation into a THF representation; THF is the
TPTP standard for classical higher-order logic, i.e. Church's simple
The main function provided is KIF2THF(KIFaxioms,KIFqueries,KnowledgeBase)
A challenge part in this transformation is the computation of an appropriate
typing for the KIF terms and formulas. This is partly non-trivial.
The conversion is intented to work purely syntactically (when no
typing-relevant information from SUMO is available) or mixed
syntactically-semantically (when typing-relevant information from
SUMO is available).
A small example:
The KIF Problem with axioms
(holdsDuring (YearFN n2009) (enjoys Mary Cooking))
(holdsDuring (YearFN n2009) (=> (instance ?X Female) (wants Ben ?X)))
(holdsDuring ?X (instance Mary Female))
(holdsDuring ?X (and (?Y Mary Cooking) (wants ?Z Mary)))
is tranlated into the THF problem:
%%% The extracted Signature %%%
%%% The translated axioms %%%
thf(ax,axiom,((! [X: $i]: (holdsDuring @ X @ (instance_THFTYPE_IiioI @ mary @ female))))).
thf(ax,axiom,((! [X: $i]: (holdsDuring @ (yearFN_THFTYPE_IiiI @ n2009) @ ((instance_THFTYPE_IiioI @ X @ female) => (wants @ ben @ X)))))).
thf(ax,axiom,((holdsDuring @ (yearFN_THFTYPE_IiiI @ n2009) @ (enjoys_THFTYPE_IiioI @ mary @ cooking)))).
%%% The translated conjectures %%%
thf(con,conjecture,((? [X: $i,Y: $i,Z: $i]: (holdsDuring @ X @ ((enjoys_THFTYPE_IiioI @ mary @ Y) & (wants @ Z @ mary)))))).
This THF problem can be solved effectively by TPTP THF compliant higher-order theorem provers.
The transformation often needs to introduce several
'copies' of KIF constants for different THF types. Therefore some constant
symbols become tagged with type information during the transformation process.
Example for tagged contant symbols above enjoys_THFTYPE_IiioI and