Rules of Inference
Rules of inference are (usually) used to infer (deduce) something new from something old, such that if the old is true then so is the new. Our purpose is just the opposite: to reduce something we hope is true to some new thing(s), such that if the new are true, then so is the old. Hence, what we call an "elimination rule" corresponds to what is usually called an "introduction rule," but applied backwards.

To illustrate this, let's consider the traditional rule for conjunction ("and") introduction: 

        P     Q
      -----------
       (P and Q)
This says that if we have proved P and Q separately, then we are entitled to say we have proved their conjunction P and Q. A better formulation is 
       A |- P     A |- Q
      -------------------
         A |- (P and Q)
where A is a set of axioms, and |- indicates first order proof. In our context, we have a goal of proving P and Q (from A), and the above tells us it suffices to prove P and Q separately; that is, we can apply the rule backwards, to eliminate the conjunction from our goal; this is why we call the rule "conjunction elimination."

The rule that is usually called conjunction elimination is completely different: it says that if we have proved P and Q, then we are entitled to say we have proved P. This may be written: 

       A |- (P and Q)
      ----------------
          A |- P
Using such traditional rules in the forward direction gives a bottom up proof: we start with what we know, and gradually build up more. By contrast, our proof planning rules build top down proofs: we start with what we want, and work down towards what we know. The most important property such a rule can have is to be semantically sound. For the above rule to be sound, the following must be satisfied: 
       A |= P     A |= Q
      -------------------
         A |= (P and Q)
where |= indicates semantic entailment, which is defined by satisfaction.

To emphasize the importance of soundness, and to indicate our backwards use of the rule, we will write our conjunction elimination in the form 

    A |= (P and Q)   ---->  A |= P and A |= Q
However, "real" proofs (e.g., from textbooks, research papers, lectures and blackboards) in general are neither top down nor bottom up! And reading a proof written in either of these styles can be pretty tedious; a proof is fun (or at least, relatively easier) to read if it is organized to tell a story. This results from the deep seated human desire for coherence through causal explanation: we want to know why a particular step is taken, not just that it happens to work. A great deal could be learned about how to present proofs from the study of narratives, particularly oral stories as actually told.

The rules below are commonly used by our tatami system; they all involve first order logic, with which we assume some familiarity - see Chapter 8 of the forthcoming book, Theorem Proving and Algebra for a systematic algebraic exposition of first order logic.

  1. conjunction elimination.
  2. implication elimination.
  3. quantifier elimination.
  4. lemma introduction.
We will not state our rules formally, but instead describe what they are for and how they are used. Formal statements can (eventually) be found in Chapter 8 of Theorem Proving and Algebra.

The following rules are treated in the tutorial on universal algebra:

  1. reduction.
  2. induction.
    3. [Next] [Home] [BHome]
    12 October 1996