Glossary

Imported Sub-Theories

The theories in the foundational ontology database are to some extent organised into a hierarchy by means of the notion of an imported sub-theory. Sub-theory relationships are declared in the theory database files using the meta-predicates:
subtheory( <parent-theory>, <sub-theory>)
and
subtheory( <parent-theory>, <sub-theory>, <restriction>).

For example the 3D version of Tarski's elementary geometry incorporates the generic nD theory as a subtheory. This is declared in the theory file tarski_geom_3D_theory.pl by the following declaration:
subtheory( tarski_geom_3D, tarski_geom_nD ).

In the HTML display for tarski_geom_3D this declaration is displayed by the entry THEORY(tarski_geom_nD) in the `Imported Sub-Theories' section of the page.

The meaning of the sub-theory declaration is simply that all the formulae from the named sub-theory are to be included as formulas in the parent theory.

The 3-ary version of subtheory is used to specify a predicate restriction on the domain that is constrained by the imported sub-theory. In other words, the sub-theory is only applied to a particular subset of the elements in the domain of the parent theory. For example the declaration subtheory( rbg, tarski_geom_3D, 'US' ) means that in the theory rbg the domain of all the elements satisfying the US predicate (the unit spheres) satisfies the axioms of the theory tarski_geom_3D.
That this means formally is that all quantification in the subtheory is limeted to the extension of the restriction predicate.
Thus all(x, PHI(x))becomes all(x, if( <res-pred>(x), PHI(x))
and ex(x, PHI(x)) becomes ex(x, and( <res-pred>(x), PHI(x))
These transformations are applied to all quantifiers in the axioms of sub-theory and the resulting restricted axioms are then added to the parent theory.