RE: SUO: RE: Re: Peirce's MS 514
Pat,
Thanks for the reference and comments on general logic and functional
programming.
With regard to the Lifschitz reference: This was based on recollection of
some things I was looking into about a year and a half ago, and it appears
that Jon was right about old memories being like old strawberries-- getting
fuzzy.
Anyhow, here is an accurate version, as far as it goes:
The only paper I was able to find in my "files" that refers to program
rules as rules of inference is
M. Gelfond and V. Lifschitz, "Classical negation in logic programs and
disjunctive databases," New Generation Computing, 1991, pp. 365-385.
which is available in postscript format at
http://www.cs.utexas.edu/users/vl/papers-old.html
This concerns extended logic programs which introduce "classical
negation" (I think these are scare quotes) in addition to negation as
failure.
The tie to my comment about inference rules is in a statement:
"Thus our semantics is not 'contrapositive' with respect to <-- and ~; it
assigns different meanings to the rules P <-- ~Q and Q <-- ~P. The reason
is that it interprets expressions like these as _inference_rules_, rather
than as conditionals. ... The language of extended programs includes
classical negation, but not classical implication." (Here ~ is the
"classical negation" operator.)
I believe there was more discussion of this somewhere in papers of either
Lifschitz or Gelfond, but I can't find it! It also appears that, contrary
to what I said in my previous message, I was the one interested in
paraconsistent logic, not Gelfond and Lifschitz. They were explicitly
_not_ interested in paraconsistent logic, since they fix things up so that
contradiction results in all literals being true, and note:
"This shows that our approach to negation is different from the
'paraconsistent' approach of [Blair and Subrahmanian 1989]."
With this much to jog my memory, I'll add a couple of things.
As I recall I didn't like this particular semantics very much, but did like
the concept of extended logic programs. (I was interested in a situation
where I could see a use for both negation as failure and statements
declared to be untrue (in some sense).) I don't have a good trace of the
path I followed, but this led me to logic with values in a bilattice
instead of in {true,false}. A major reference for this is "Multivalued
Logics" by Matthew L. Ginsberg, available at
ftp://ftp.cirl.uoregon.edu/pub/users/ginsberg/papers/ as mvl.ps.gz.
This allows an approach to paraconsistent logic that has a nice structure
to it, and provides a basis for better understanding of the issues of
implication and several different versions of negation.
The bilattice approach was tied back into extended logic programming and
paraconsistency by, among others, Avron and Arieli. For example,
"A Model-Theoretic Approach to Recover Consistent Data from Inconsistent
Knowledge-Bases," available at http://www.math.tau.ac.il/~aa/papers.html
This has become off topic, although some of it may be relevant to
rationalizing different ontologies. :-)
Just one more thing, since I've come this far:
A somewhat different approach to extended logic programming is (NB:
IIRC) in the work of Alferes, Pereira, Damasio. Apparently based in part
on this work, recent versions of XSB (a research oriented extension of
Prolog, http://www.cs.sunysb.edu/~sbprolog/xsb-page.html) come with an
interpreter for which it is said "We note in passing that WFSX programs can
be paraconsistent." (Users manual, vol2, 1.1.12, Extended Logic Programs)
John V.
>
>
>>The contributions of John S, Pat Hayes, Chris Menzel and
>>others to this thread have helped clarify a lot of
>>things that I thought I already understood. A short
>>footnote to Pat's note--
>>
>>It is also amazing that there is such a large variety
>>of useful (not necessarily complete) inference systems,
>>involving various combinations of axioms,
>>axiom schemata, and rules of inference. If
>>one has only axioms, and no rules of inference, the theory
>>is only the axioms (using theory to mean the body of
>>statements that can be inferred, not the totality of
>>what is entailed.) In logic programming, the rules in a
>>program are usually regarded as axioms (insofar as we're
>>speaking of rules with only logical intent). In extending
>>prolog to a certain version of paraconsistent logic
>>Vladimir Lifschitz proposes instead to regard the
>>rules as rules of inference. This provides a completely
>>new perspective on the 'meaning' of the logic programs
>>in question.
>
>Thanks for that note. Do you have a pointer to this work by Lifschitz?
>
>There is a tradition called 'general logic' of rendering rules (of
>inference) as assertions in another logic with a simpler or more
>uniform system of rules. This has a lot in common with implementing
>one virtual machine in another one, and many ties with computability
>theory. In particular, there is a kind of uniform technique for
>mapping many systems of rules into a 'universal logic' of functional
>type theory - essentially, the lambda calculus with a sorted
>functional syntax. The expressions of the orginal language map into
>types, and the inference rules map into functions. Applying a rule
>maps into a function call, where the type-matching of a function to
>its arguments encodes the particular syntactic structures of the
>original language. One can then think of this functional language as
>a general-purpose meta-calculus for building *proofs* in the original
>language; in other words, derivations map into terms. This makes
>sense if you think of an inference rule as an operation on
>derivations which 'outputs' a larger derivation when given smaller
>ones as 'input', and you think of an expression as simply being a
>kind of runty derivation (of itself from itself). See
>http://www.dcs.ed.ac.uk/home/cdw/archive.html
>and follow the links there for more information than one human brain can
>hold.
>
>Pat Hayes