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 <[EMAIL PROTECTED]> 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.
