Include File Name Space Hierarchy

by Tobias Gleißner Alex Steen, Geoff Sutcliffe,

Motivation

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.

Proposal

include directives get an optional third argument that names the space for the formulae in the included file.
The second argument that lists the formulae to be included from the file can be a (possibly empty) list or a * to mean "all formulae".
As before, an included file can include another file, and now can give a name for that (sub)space.
If a hierarchy of spaces in included, the symbols in the hierarchy have the hierarchy of space names prepended, separated by |||.
In proofs, the formula names have the hierarchy of space names prepended, separated by |||.

For example:

---- MyProblem.p ----

include('TopSpace.ax',*,top).
include('BtmSpace.ax',[],useless).  %----Just to show you can import nothing
fof(an,axiom,p(a)).
fof(an,conjecture,p(a) & 'top|||q'(b) & 'top|||btm|||r'(c)).

---- TopSpace.ax ----

include('BtmSpace.ax',[r],btm).
fof(an,axiom,! [X] : ( q(X) => 'btm|||r'(X) ) ).

---- BtmSpace.ax ----

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)).
fof(2,plain,$false,
    inference(magic,[status(thm)],[an,'top|||an','btm|||another'])).

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.