On Mar 15, 2007, at 5:41 PM, Daniel J McGoldrick 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
No use wasting time trying to get both in a perfect Panglosian
world :-).
[snip]
Except many logics, and I would say nigh all computational logics, do
have sound and complete proof systems. Indeed, many logics (e.g., OWL
DL) have *decision procedures*. Among logics with s&c proof
procedures is first order predicate logic as shown by.....Godel:
http://en.wikipedia.org/wiki/Gödel's_completeness_theorem
Establishing certain metalogical properties of a formalism does not
settle the properties of an implementation of that formalism, so
testing (and other verification techniques) are still required. And,
of course, if you lack a decision procedure (as with FOL), then there
are certain answers your implementation won't get, so again care is
needed. And with expressive decidable logics, the high worst case
complexity can kill you.
And of course, some times, approximation is good enough. But, in
general, it's nice to have a formalism that is well behaved,
computationally and mathematically, and if not computationally, at
least mathematically, because such formalisms are better understood
overall.
Cheers,
Bijan.
