Include File Name Space Hierarchy
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
- 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 |||.
---- MyProblem.p ----
include('BtmSpace.ax',,useless). %----Just to show you can import nothing
fof(an,conjecture,p(a) & 'top|||q'(b) & 'top|||btm|||r'(c)).
---- TopSpace.ax ----
fof(an,axiom,! [X] : ( q(X) => 'btm|||r'(X) ) ).
---- BtmSpace.ax ----
fof(an,axiom,! [X] : ~q(X)).
---- 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.