SUO: Re: Internal Consistency proof?
Pat,
This is a good idea. All we need to do is create more mature theorem
proving software that can be installed easily and run without
supervision. A simple matter of programming as they say!
Adam
At 11:41 AM 5/3/2003 -0400, Patrick Cassidy wrote:
>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
>=============================================