Re: Goedel's incompleteness theorom?

Daniel --

"Sound and complete" is sometimes used to mean "may run forever and will
find all correct answers, but won't tell you when that has happened".

What's usually needed in practical reasoning systems is "sound, complete,
and terminating", -- and of course, efficient.

This is possible for useful subsets of logic.  The paper

   Backchain Iteration: Towards a Practical Inference Method that is Simple
   Enough to be Proved Terminating, Sound and Complete. Journal of Automated
Reasoning, 11:1-22**

is one example, and it forms the basis for a Wiki-like system.  The system
is online, with medical and other examples, at the site below.

Apologies to those who have seen this before, and thanks for comments.

                                                 -- Adrian

** If this is of interest, I'll be glad to send you a copy

Internet Business Logic
A Wiki for Executable Open Vocabulary English
Online at www.reengineeringllc.com    Shared use is free

Adrian Walker
Reengineering



On 3/15/07, Daniel J McGoldrick <djmcgoldrick@comcast.net> wrote:
>
>  Hello --
>
> I have been following the public-semweb-lifesci discussions
> for some time (silently) with great interest.  By way of introduction, I
> am the CEO and founder of Sentient Solutions Inc. - a non-profit Colorado
> company with an affiliated Consulting LLC Sentient Consulting. I
> worked for UC-computational pharmacology for four years, and for
> Evolutionary Genomics.
>
> I thought I would chime in for a brief moment. "Sound and Complete"  i.e.
> consistent and complete is proven impossible by Gödel - see
>
> http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorem<http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorem>
>
> No use wasting time trying to get both in a perfect Panglosian world :-).
>
> but... if the reasoning systems we have on closed world systems (using
> equality, transitive closure and other formal rules of logic) have enough
> apriori  *validation tests*, we can achieve
> something very close. Are the inferences right? Are the facts consistent?
> Are the answers biologically supported? Hammering
> each inference with apriori validity tests (same chromosome,
> same gene, not deprecated, not homonymous...) the "lies"
> or inconsistencies can be flushed out to a certain level of significance
> and removed or marked in the graph of triplets that the reasoners use.
>
>  Completeness is a function of how many triplets can be inferenced over by
> a reasoner with rules, and also a data integration challenge...
>
> Then, I find that the triplet stores become huge, slow to compute over and
> the reasoners become slow for larger A-boxes.  The quality of the answers
> can be validated by simple logic with a nice list of tests though, and not
> too surprising, inconsistencies in the logic happen just as Gödel predicts.
>
> Then wouldn't the question be how to identify the erroneous triplets and
> repair them in the overall triplet graph retaining as complete of a graph
> and thus inferencing capability as possible?
>
> Daniel J McGoldrick Ph.D.
> Sentient Solutions Inc.
>
>
>