Include File Name Space Hierarchy

by Tobias Gleißner Alex Steen, Geoff Sutcliffe,


Tobias' interests are combining ontologies (which make heavy use of namespacing) and (nonclassical) logics in general but also specifically in legal reasoning. He believes that we somehow need predefined domain terminology and some background knowledge about the terminology which is easy to handle like OWL in Protégé for bringing more automated reasoning into industry.


For example:

---- MyProblem.p ----

include('',[],useless).  %----Just to show you can import nothing
fof(an,conjecture,p(a) & 'top|||q'(b) & 'top|||btm|||r'(c)).
---- ----
fof(an,axiom,! [X] : ( q(X) => 'btm|||r'(X) ) ).
---- ----
fof(an,axiom,! [X] : ~q(X)).
fof(another,axiom, r(c)).
---- Refutation.txt ---
fof(1,negated_conjecture,~p(a) | ~'top|||q'(b) | ~'top|||btm|||r'(c)).

It is easy to preprocess a hierarchical include into a regular TPTP file using ''ed flat names, so that existing tools don't have be radically changed. In contrast, adding a new form of symbol with a ||| separated structure would cause a lot of work for system developers ... if they don't do it then you have nothing.