SUO: Internal Consistency proof?
Just a thought about the problem of internal consistency:
Adam Pease mentioned in his discussion of experience with SUMO:
> ... as well as being impossible in practice on theories of
> any significant size, we have done proofs for consistency
> within specified time boundaries. We found and removed
> inconsistencies found in up to 50-step proofs. We can run
> for days now without finding anything, so we have some
> degree of confidence that SUMO is internally consistent.
If the size and structure of some module or combination of
modules of an ontology makes it impractical to prove internal
consistency in days of computing, perhaps that task can
be designed, like the SETI screen saver, to run in
the background and parts of the task distributed to willing
ontologists to get as much confidence as possible in any
given ontology. It is understood that each new axiom
would require another round of computing, but for any
given proposed SUO, our group might in this way find
some probabilistic confidence measure for the logical
consistency, though not the utility, of a proposed
standard.
Would creating such a background consistency-checker
be an appropriate task for someone involved in
the SUO? I myself am clueless as to how to do it.
But I would be willing to retire my SETI screen saver
and let my machine run consistency proofs on any
proposed standard. Does this make any sense?
Pat
=============================================
Patrick Cassidy
MICRA, Inc. || (908) 561-3416
735 Belvidere Ave. || (908) 668-5252 (if no answer)
Plainfield, NJ 07062-2054 || (908) 668-5904 (fax)
internet: cassidy@micra.com
=============================================