Hello John, (01)
John A. Bateman wrote: (02)
>
>
> Structuring is even more crucial for proving consistency of
> ontologies. It is much easier to prove inconsistency (i.e.
> derive false using a theorem prover) than prove consistency
> (e.g. by constructing a finite model using a SAT solver, or
> by using a resolution prover for finding a saturated set of
> clauses not containing the empty clause). (03)
Consistency proofs can also be done in the metatheory by characterizing
all possible models of a theory and classifying them up to isomorphism.
This is what we have done with the PSL Ontology.
For each theory within the ontology, we specify a class of structures and
then prove two theorems:
Satisfiability: any structure in the class satisfies the theory.
Axiomatizability: any model of the theory is elementarily equivalent to
a structure in the class. (04)
It is definitely easier to prove the Satisfiability and Axiomatizability
Theorems
for a modular ontology than for an unstructured ontology. (05)
In fact, we have used this approach to explicitly identify the modular
theories within an ontology -- a module is a minimal set of axioms
needed to prove the Satisfiability and Axiomatizability theorems
for the class of structures that captures the intended semantics of a
relation
or set of relations. (06)
> We did not manage to
> prove consistency of DOLCE with such techniques, and have
> just prepared a grant proposal that proposes to use structuring
> techniques (e.g. the Robinson joint consistency theorem).
> The crucial problem here is to develop techniques for establishing
> conservativity of theory extensions. (07)
Extensions may be nonconservative, and theories in the ontology may be
mutually inconsistent. For example, Discrete Time and Dense Time are
nonconservative extensions of Linear Ordered Time that are mutually
inconsistent. (08)
A nontrivial example from PSL is that the core theory occtree.th is a
nonconservative extension of PSL-Core. The latter theory allows finite
models in which some activities have no occurrences, whereas the former
theory
does not (since its models contain all sequences of occurrences of all
activities). (09)
- michael
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/uos-convene/
To Post: mailto:uos-convene@xxxxxxxxxxxxxxxx
Community Portal: http://ontolog.cim3.net/
Shared Files: http://ontolog.cim3.net/file/work/UpperOntologySummit/uos-convene/
Community Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?UpperOntologySummit (010)
|