**Mail folder:**Interlingua Mail**Next message:**sowa@watson.ibm.com: "Peirce's rules of inference"**Previous message:**sowa@watson.ibm.com: "Peirce's rules of inference for existential graphs"**In-reply-to:**sowa@watson.ibm.com: "Peirce's rules of inference for existential graphs"

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