On Thu, Mar 09, 2006 at 01:04:24PM -0500, Michael Gruninger wrote:
> >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).
>
> Consistency proofs can also be done in the metatheory by characterizing
> all possible models of a theory and classifying them up to isomorphism. (01)
Michael, I may be misunderstanding (been known to happen :-), but how
does such a classification yield consistency? From the fact that you've
partitioned the models of theory T into isomorphism classes (I take it
this is what you mean by "classifying them up to isomorphism") it
doesn't follow that there *are* any such models. Granted, it may be
obvious in some cases that there are, but if the specification of a
model is complicated enough, it may not be. (02)
> 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. (03)
But again, consistency doesn't follow from satisfiability in this sense
alone (so "satisfiability" might actually be a misnomer here). We also
need to know that the class of structures in question is nonempty.
Fortunately, as you know better than anyone, in the case of PSL, you can
prove (in ZF) that the relevant class is nonempty pretty easily. But,
conceptually anyway, that's a separate proposition that might, in
general, require a distinct proof. (04)
-chris (05)
_________________________________________________________________
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 (06)
|