Re:Peirce's rules of inference for existential graphs
phayes@herodotus.cs.uiuc.edu
Message-id: <9208280153.AA18905@herodotus.cs.uiuc.edu>
Date: Thu, 27 Aug 1992 20:55:52 -0600
To: sowa@watson.ibm.com
From: phayes@herodotus.cs.uiuc.edu
Subject: Re:Peirce's rules of inference for existential graphs
Cc: INTERLINGUA@ISI.EDU, SRKB@ISI.EDU, CG@CS.UMN.EDU
John,
An interesting collection of observations. However, a few brief comments.
First, your comparison with resolution doesnt seem quite fair, since you
include the cost of transforming from Fregean notation to clausal form,
whereas you ignore the cost of transforming from it to Pierce's notation.
(And by the way, how do you get the figure of eleven steps to do that
conversion? This suggests that this conversion is an inference process,
whereas it is of course a simple algorithm which involves no search or
heuristics, and can be made to happen extremely quickly.) Theorem-proving
folk quite rapidly get used to writing axioms in clausal form, so that
Prolog for example is written in Horn clauses, as you know. Therefore if we
compare the resolution world to Pierce's, we find that the proof of
proposition 3.47 is rather shorter in resolution than in Pierce's notation.
But moreover, crucially for computation, it is conservative: that is, at no
step is the inference process required to introduce a new symbol,
exercising creativity. That was exactly the great advance that resolution
represented over earlier theorem-proving methods, since without this
property, the machine must seach through the Herbrand universe, a hopeless
task. Starting from a blank sheet of paper is a recipe for disaster in a
mechanical system.
While you correctly observe that clausal form sometimes looks rather unlike
the nonclausal version of an expression, there are two quite reasonable
replies to this. One is that this doesn't matter in practice (cf. Prolog).
The other is that what makes clausal form sometimes rather unnatural is
that it involves distributive 'multiplication' of AND over OR. But it is
fairly easy to define a less awkward normal form which has negations pushed
inwards using DeMorgans laws but does not do this distribution, and
redefine resolution on that form. This is rarely done for the first reason,
but see D. Wilkins, "A nonclausal theorem-proving system", 1st AISB
conference 1974. Wilkins system has the 'remarkable property' you mention,
of allowing inferences to move down many depths of nesting.
You say that Pierces graphs have no variables, but you don't tell us how
then they express quantification. Your account leaves them with only
propositional expressibility.
Can a 'context' contain more than two graphs? For example, how does the
notation express p&q&r&s ? If it does it by simply writing p q r s on the
plain paper, then you don't need the negation prefix ^ at all, since it is
implicit in the bracketing. That simplifies the notation somewhat.
Finally, I protest at your usage of the word 'context' here. This word is
rapidly getting covered with more confusion than 'state' or even
'ontology'. Even in your brief message it has several meanings. First, it
means something like the scope of a negation sign, ie a subexpression. But
you also imply that it has some operational significance, so that a
'context' somehow restricts the attention of a search process:
>Furthermore, they allow graphs to be imported
>into a small context where only the information relevant to a proof
>needs to be considered.
But this is quite misleading. By the very permissive nature of the
importation rule, these 'small' contexts can be made as large as we like.
There is nothing in the inference system to keep them small. They are
merely scopes of negation symbols. If we translate Pierce's notation into a
simpler form by pushing all negations inwards, we get a notation consisting
of dual clausal form, with all this 'context' structure eliminated. The
infernce search problem is exactly the same as it was before we did this
translation: every inference we can now do has a corresponding inference we
could do previously. (In fact, since this translation can be done using
Pierce's rules, we can regard the process of performing this simplification
as the utilisation of a certain proof-theoretic normalisation theorem which
simpifies the search space: do all inferences of type A before any of type
B.)
Look at Pierce's version of your example ( I omit '^' )
[ [p [r]] [q [s]] [ [p q [r s]] ] ]
Apply double-negation elimination twice and we get
[p[r]] [q[s]] p q [rs]
which is simply the dual of the clausal form
^p|r, ^q|s, p, q, ^r|^s.
Surely, to apply double-negation elimination wherever possible might seem
to be a useful heuristic. In general, these 'contexts' just create
difficulty in the search process.
The theorem-proving community has developed a useful set of technical ideas
for analysing the search properties of logical spaces. Talk of the
'structure of encapsulated contexts' where 'only the information relevant
to a proof
needs to be considered' just creates confusion. If we have some way of
knowing what information is relevant to a proof, we can use it in any
normal form we like. And to think that a notation will control exponential
growth of search spaces by allowing 'large problems to be broken down into
smaller contexts' is just fantasy.
Pat
----------------------------------------------------------------------------
Pat Hayes <through 1992>
Beckman Institute (217)244 1616 office
405 North Mathews Avenue (217)328 3947 home
Urbana, Il.61801 hayes@cs.stanford.edu (217)244 8371 fax