Proof Trees as Formulas

Claus-Peter Wirth

Dept. of Computer Sci., Universität des Saarlandes, D–66123 Saarbrücken, Germany

                              wirth@logic.at

Abstract. This draft is for internal communication and not completely self-contained.

1 Motivation

On the one hand, proof trees like sequent or tableau trees are very useful for formalizing a logic and for administrating the state of proof attempts in an implementation. Moreover, with proof trees it is easily possible to have a simple rule-based local means of specifying the possible deductive inference steps. Such a specification consisting of a set of local inference rules is not only well-suited for communicating a logic between human beings. It can also be used to include the logic into a logical framework, provided that the framework directly and conveniently supports the typical inferences of the logic.

On the other hand, in spite of their conceptual clearness, these proof trees still put off possible users of theorem provers who do not have an education that includes logic calculi, like many mathematicians and most engineers and students of computer science. Experience shows that while a growing group of possible users of a theorem prover are well acquainted with formulas expressing proof obligations and have a clear intuitive understanding of their semantics, they are not thinking in terms of a formal calculus, they do not want to think in terms of proof trees, and it takes them quite a while until they find it natural to formulate and understand proofs in the form of formal proof trees; and with the more efficient matrix representations of these proof trees, only a very small number of scientists feel comfortable.

Bringing both hands together, it would thus be nice to combine the advantages of proof trees with the possibility to present proof trees in the form of formulas that resemble the structure of the input formulas as closely as possible. Inspired by [1] (which combines and significantly extends ideas from [3–5]), we want to present here a first step into this direction.

For simplicity we restrict ourselves to classical logic and use the convenient sequent style presentation in this paper, although an implementation should use structure-sharing matrix techniques.

2 Introduction

The basic idea is roughly as follows.

Instead of applying inference rules to an original sequent (i.e. a disjunctive list of formulas), the user points at a certain position in a formula in order to set the focus of his proof to the subformula pointed at. The sequent calculus in the background applies the minimum number of calculus steps in order to make this position to a top position of a formula of a sequent of the proof tree and the resulting sequent is presented to the user in an appealing format. Optionally, all formulas in the sequent with the exception of the one pointed at may be further decomposed as long as α-, δ-, or γ-steps (according to Smullyan’s classification) are applicable to them. Note that, while the β-steps cannot be handled this way because they split the sequent in twain, the automatic decomposition of α-, δ-, and γ-formulas cannot provide any difficulties when the δ-steps are liberalized ones, and when the γ-steps are limited to a multiplicity of 1 and use free variables. Now the user can globally instantiate free variables in order to get complementary formulas (in which case the whole sequent will be replaced with the single-formula sequent ‘true’), use equations &c. for contextually rewriting those formulas pointed at, or make a case analysis (implemented as Cut), or replace a redundant formula pointed at with the formula ‘false’. He can also set additional pointers to subformulas in order to trigger further decomposing calculus steps.

So far this looks very much like a traditional sequent calculus with a nice mouse-clicking user interface. The additional feature here, however, is the possibility to remove the previously set pointers either completely or otherwise to a parent position. In this case, the sequent calculus steps are undone in a way that respects the changes that have taken place between setting and removing the pointer. E.g., if a sequent has turned into true, this branch of the proof tree will be cut off when undoing the sequent calculus steps. A proof is successfully finished when all pointers have been removed and the current sequent reads ‘true’. If the result is not ‘true’ because the original formula was not valid, our proof attempt may nevertheless be useful because the resulting sequent is equivalent to the input sequent, and hopefully simpler.

3 Automatic Simplification

We define a sequent to be a list of formulas. Note that we will make use of the ordering of the formulas in the list insofar as the number of a formula—counting from right to left—will be used to identify it even after transformations and addition of new formulas to the left end of the sequent.

We use upper case Greek letters to denote sequents, upper case Latin letters to denote formulas, and lower case Latin letters to denote terms.

The conjugate of a formula A (written: \overline{A} ) is the formula B if A is of the form ¬B, and the formula ¬A otherwise. In this paper we add one additional exception for formulas of the form (A_{0} ∨ … ∨ A_{n+1}) in which the ‘∨’ is annotated to be soft w.r.t. conjugation, as introduced by our γ-rules of Section 4.4.

In this case we recursively define \overline{(A_{0} ∨ … ∨ A_{n+1})} = ( \overline{A_{0}} ∧ … ∧ \overline{A_{n+1}} ), where also the ‘∧’ is annotated to be soft, with an analogous definition of the conjugate.

We assume that formulas are immediately normalized w.r.t. the following confluent and terminating rewrite system. Note that, although preservation of the original formula structure is very important for user interaction and is a major subject of this paper, we are only interested in preservation of the formula structure modulo a simple form of simplification.

false ∨ A  → A
A ∨ false → A
true ∨ A  → true
A ∨ true → true
A ∨ A  → A
A ∨ ¬A → true
¬A ∨ A  → true

false ∧ A  → false
A ∧ false → false
true ∧ A  → A
A ∧ true → A
A ∧ A  → A
A ∧ ¬A → false
¬A ∧ A  → false

false ⇒ A  → true
A ⇒ false → ¬A
true ⇒ A  → A
A ⇒ true → true
A ⇒ A  → true
A ⇒ ¬A → ¬A
¬A ⇒ A  → A
false ⇐ A  → ¬A
A ⇐ false → true
true ⇐ A  → true
A ⇐ true → A
A ⇐ A  → true
A ⇐ ¬A → A
¬A ⇐ A  → ¬A

false = A  → ¬A
A = false → ¬A
true = A  → A
A = true → A
A = A  → true
A = ¬A → false
¬A = A  → false

¬false → true
¬true → false
¬¬A → A

(t=t) → true

Actually, we write ∧ and ∨ as lists of associative operators and the last three rewrite rules for each of these operators are to be understood modulo associativity and commutativity.

Moreover, the resulting sequents are always immediately rewritten at most one step via

Γ true Π  → true
Γ A Δ ¬A Π → true
Γ ¬A Δ A Π → true

The latter two rules should also apply when the two occurrences of A actually differ but can be unified by setting free γ-variables that do not occur in other leaf sequents. They even should trigger automatic α-, γ-, and δ-decomposition in order to be applicable.

Finally, we rewrite inference steps in proof trees according to the confluent and terminating rewrite system:

\frac{Γ}{true}  → \underline{true}
\frac{Γ}{Π_{0} ⋯ Π_{m−1} true Δ_{0} ⋯ Δ_{n−1}}  → \frac{Γ}{Π_{0} ⋯ Π_{m−1} Δ_{0} ⋯ Δ_{n−1}}

Note that in the last rewrite rule each of the ‘Π_{i}’, ‘Δ_{j}’, ‘true’ denotes a separate sequent, not a part of a long concatenated sequent. Note that in the good old days when trees grew upwards, Gerhard Gentzen would have inverted the inference rules such that passing the line means consequence. In our case, trees grow downwards and passing the line principally means reduction, but actually equivalence transformation.

We will call this whole rewrite system automatic simplification.

While the latter tree rewriting part of automatic simplification may be hard wired, the formula rewriting part should be programmable by the logics programmer, but not by the user of the theorem prover.

4 Inference Rules

It should be clear that any inference rule now comes as a single decomposition rule (↓) as usual, plus a list of rules (↑) for recomposition whose applicability is tested in the precedence from left to right when the step has to be undone.

Note that the ↓ and ↑ do not indicate any direction of consequence. All our inference rules will be equivalence transformations.

In general, we will use “↑ id” as an abbreviation for the rule

↑ \frac{Ξ′}{Ξ′}

that asks just to hand up the lower sequent as upper sequent on recomposition, provided that this rule is applicable, which is the case when there is exactly one lower sequent

4.1 α-Rules

Let us consider some α-rules first. As double negation does not occur according to automatic simplification, all our α-rules have at least two side formulas.

↓ \frac{Γ (A_{0}∨ … ∨A_{n+1}) Π}{Γ A_{0} … A_{n+1} Π} ↑ \frac{Ξ′ (A′_{0}∨ … ∨A′_{n+1}) Π′}{Ξ′ A′_{0} … A′_{n+1} Π′}

Note that, due to automatic simplification, this means that when we undo the decomposition of an α-formula and the lower sequent has been simplified to ‘true’, we do not apply the ↑-rule since the rewriting of automatic simplification will already have removed the whole inference step.

Note that the recomposition step (↑) will trigger automatic simplification for those A′_{i} that have become false.

In any case, on recomposition we only put the formula back to its old position in order to be able to preserve the structure of the original sequent when removing all pointers.

Technically, the whole decomposition and recomposition can be achieved the following way: When we apply the ↓-rule we annotate the inference step with n+1 and with the number that indicates the position (say p) of the principal formula say (A_{0}∨ … ∨A_{n+1}) in the upper sequent (numbering from right to left). When we apply the corresponding ↑-rule we remove the formulas number p+n+1, …, p, join them with the operator ∨ into an ∨-formula, and insert it at position p. Thus, we require in the above rule as well as in the below rules that the number of formulas of Π is equal to the number of formulas of Π′.

In a matrix representation the technical realization would be as follows. Γ (A_{0}∨ … ∨A_{n+1}) Π would be represented as a list of positions (path) in the original sequent say g_{m}, …, g_{1}, a, h_{p}, …, h_{0}, and the new path would be

g_{m}, …, g_{1}, a0, …, a(n+1), h_{p}, …, h_{1},

representing the lower sequent.

More α-rules:

↓ \frac{Γ ¬(A_{0}∧ … ∧A_{n+1}) Π}{Γ \overline{A_{0}} … \overline{A_{n+1}} Π} ↑ \frac{Ξ′ ¬(\overline{A′_{0}}∧ … ∧\overline{A′_{n+1}}) Π′}{Ξ′ A′_{0} … A′_{n+1} Π′}

↓ \frac{Γ (A⇒B) Π}{Γ \overline{A} B Π} ↑ \frac{Ξ′ ( \overline{A′} ⇒B′) Π′}{Ξ′ A′ B′ Π′}

↓ \frac{Γ (A⇐B) Π}{Γ A \overline{B} Π} ↑ \frac{Ξ′ (A′⇐ \overline{B′}) Π′}{Ξ′ A′ B′ Π′}

4.2 Liberalized δ-Rules

↓ \frac{Γ ∀x. A Π}{Γ A\{x↦x^{δ}\} Π} V_{free}(A) × \{x^{δ}\} ↑ id

Note that this rule requires a semantics for free variables (as the one in [7]) to make sense. The x^{δ} is a new free δ-variable, which serves as a special parameter in an equivalence transformation. The V_{free}(A) × {x^{δ}} to the right has to be added to the current variable-condition, which takes care of the soundness. Roughly speaking, this means that the free γ-variables in A must not be instantiated with terms that contain x^{δ}.

More γ-rules:

↓ \frac{Γ ¬∃x. A Π}{Γ \overline{A\{x↦x^{δ}\}} Π} V_{free}(A) × \{x^{δ}\} ↑ id

4.3 Unconditional Contextual Rewriting

Let s and t be either both terms (of the same type) or both formulas. Assume that the formula B is listed in the sequent Γ Π. Let A[t] denote the formula A[s] with some occurrences of s replaced with t. Now we can apply the rule

↓ \frac{Γ A[s] Π}{Γ A[t] Π} ↑ id

in any of the following cases:

1. B is one of the formulas (s≠t) or (t≠s).

2. B is s and t is false.

3. B is ¬s and t is true.

The latter two kinds of rewriting should actually be part of automatic simplification for the case that A[s] is the formula focused on.

4.4 γ-Rules

↓ \frac{Γ ∃x. A Π}{Γ ∃x. A A\{x↦x^{γ}\} Π} ↑ \frac{Ξ′ (A′_{0}∨A′_{1}) Π′}{Ξ′ A′_{0} A′_{1} Π′}

Note that in a matrix representation or indexed formula tree we have to change the subformula ∃x. A destructively into (∃x. A ∨ A{x↦x^{γ}}) before we then go down into A{x↦x^{γ}}.

More γ-rules:

↓ \frac{Γ ¬∀x. A Π}{Γ ¬∀x. A \overline{A\{x↦x^{γ}\}} Π} ↑ \frac{Ξ′ (A′_{0}∨A′_{1}) Π′}{Ξ′ A′_{0} A′_{1} Π′}

Note that the newly introduced ‘∨’ are soft w.r.t. conjugation in the sense that the complement operator should turn it into a soft ‘∧’ and recurse on the arguments. Otherwise the formula say

∀x. A ⇒ B

may look like

¬(¬∀x. A ∨ A′) ⇒ B

after setting and subsequently removing a focus to A, whereas it should read

( ∀x. A ∧ \overline{A′} ) ⇒ B.

4.5 β-Rules

A naïve version of a β-rule is the following one:

↓ \frac{Γ (A_{0}∧ … ∧A_{m+1}) Π}{Γ A_{0} Π ⋯ Γ A_{m+1} Π} ↑ id ↑ \frac{Γ′ ( A′_{0}∧ … ∧A′_{m′} ) Π′}{Γ′ A′_{0} Π′ ⋯ Γ′ A′_{m′} Π′}

Here we must point out a serious problem. The β-rules are the trouble-makers in logic. Not only do they (under assistance of the γ-rules) render classical firstorder logic undecidable; they also made problems in Section 2 with automatic decomposition; and now they even may not admit structure preserving ↑-rules:

Note that the above ↑-rule does not tell us what to do when at least two of the lower sequents are not ‘true’ and they differ in more than the former side-formulas, i.e. when they differ in Γ′ or Π′ !

When we only admit a single focus or a list of pointers that are on a single path in the original sequent, then we know that all transformations (besides instantiations and automatic simplification, which are global and change both sides simultaneously) will take place outside Γ and Π.

Another even more impractical solution with which we can also transform formulas in Γ Π is to undo all proof steps in this branch of the proof tree on recombination unless the modified branches turned out to be ‘true’. (This can be realized simply by taking the upper sequent and applying all global variable instantiations to it.)

Note that it is not the problem here to combine two sequents. This can always be achieved according to

↑ \frac{Γ ( ⋁ Δ_{1} ∧ ⋁ Δ_{2} )}{Ξ_{1} Ξ_{2}}

where Γ lists the formulas common to Ξ_{1} and Ξ_{2} and where Δ_{1} and Δ_{2} list the remaining formulas of Ξ_{1} and Ξ_{2}, resp.. The problem, however, is that with such a ↑-β-rule we lose all the positional correspondences and, when we remove all pointers, end up with a completely different sequent, which has no structural correspondence to the input sequent, not even modulo simplification.

Thus, in order to be useful in practice, we need a solution that is a little more involved. We define the intersection and the difference of two sequents A_{m} … A_{0} and B_{n} … B_{0} (m, n ∈ N) as the sequents C_{k} … C_{0} and D_{m} … D_{0}, resp., where k := min{m, n}, and for i ⪯ k and j ⪯ m:

C_{i} := \{ \begin{matrix}A_{i} & if A_{i} = B_{i} \\ false & otherwise \end{matrix}
D_{j} := \{ \begin{matrix}A_{j} & if n ≺ j or B_{j} = false \\ false & otherwise \end{matrix}

The intersection of several sequents is their pairwise intersection, which is associative and commutative. The formula of the sequent A_{m} … A_{0} is the formula (A_{m}∨ … ∨A_{0}), normalized w.r.t. automatic simplification, and with the ‘∨’ being soft w.r.t. conjugation.

Note the following: Let Φ be the intersection of Γ with other sequents Π_{0}, …, Π_{q}. Let Δ be the difference of Γ and Φ. Then ΔΦ is equivalent to Γ. Thus, due to distributivity of ∨ over ∧ we get the following β-rule:

↓ \frac{Γ (A_{0}∧ … ∧A_{m+1}) Π}{Γ A_{0} Π ⋯ Γ A_{m+1} Π}

↑ id ↑ \frac{Γ′′ ( (A′′_{0}∧ … ∧A′′_{m′}) ) Π′′}{Ξ′_{0} Γ′_{0} A′_{0} Π′_{0} ⋯ Ξ′_{m′} Γ′_{m′} A′_{m′} Π′_{m′}}

where the numbers of formulas of each of Γ, Γ′_{0}, …, Γ′_{m′}, Γ′′ as well as the numbers of formulas of each of Π, Π′_{0}, …, Π′_{m′}, Π′′ are the same, resp., where Γ′′Π′′ is the intersection of Γ′_{0}Π′_{0}, …, Γ′_{m′}Π′_{m′}, and where A′′_{j} is the formula of the sequent resulting from appending A′_{j}, Ξ′_{j}, and the difference of Γ′_{j}Π′_{j} and Γ′′Π′′, for j ⪯ m′.

Note that due to automatic simplification on recomposition, none of the lower sequents is true and we have m′ ⪰ 0.

With the same condition we get the following β-rule:

↓ \frac{Γ ¬(A_{0}∨ … ∨A_{m+1}) Π}{Γ \overline{A_{0}} Π ⋯ Γ \overline{A_{m+1}} Π}

↑ id ↑ \frac{Γ′′ ¬( \overline{A′′_{0}}∨ … ∨ \overline{A′′_{m′}} ) Π′′}{Ξ′_{0} Γ′_{0} A′_{0} Π′_{0} ⋯ Ξ′_{m′} Γ′_{m′} A′_{m′} Π′_{m′}}

With the analogous conditions we get the following β-rules:

↓ \frac{Γ ¬(A_{0}⇒A_{1}) Π}{Γ A_{0} Π  Γ \overline{A_{1}} Π}  ↑ id ↑ \frac{Γ′′ ¬( A′′_{0}⇒ \overline{A′′_{1}} ) Π′′}{Ξ′_{0} Γ′_{0} A′_{0} Π′  Ξ′_{1} Γ′_{1} A′_{1} Π′_{1}}

↓ \frac{Γ ¬(A_{0}⇐A_{1}) Π}{Γ \overline{A_{0}} Π  Γ A_{1} Π}  ↑ id ↑ \frac{Γ′′ ¬( \overline{A′′_{0}}⇐A′′_{1} ) Π′′}{Ξ′_{0} Γ′_{0} A′_{0} Π′_{0}  Ξ′_{1} Γ′_{1} A′_{1} Π′_{1}}

Finally, note that there are more powerful, asymmetric versions of β-rules which have shown to be useful in practical applications, e.g. with the QuodLibet system, [2]. We present only one for the ∧-formula that folds down to the right:

↓ \frac{Γ (A_{0}∧A_{1}) Π}{Γ A_{0} Π  Γ (A_{1}⇐A_{0}) Π}  ↑ id ↑ \frac{Γ′′ ( A′′_{0}∧A′′_{1} ) Π′′}{Ξ′_{0} Γ′_{0} A′_{0} Π′_{0}  Ξ′_{1} Γ′_{1} A′_{1} Π′_{1}}

4.6 Cut

↓ \frac{Π}{A Π \overline{A} Π}  ↑ id  ↑ \frac{(A′′_{0}∧A′′_{1}) Π′′}{Ξ′_{0} Π′_{0}  Ξ′_{1} Π′_{1}}

where the numbers of formulas of each of Π, Π′_{0}, Π′_{1}, Π′′ are the same, where Π′′ is the intersection of Π′_{0} and Π′_{1}, and where A′′_{j} is the formula of the sequent resulting from appending A′_{j}, Ξ′_{j}, and the difference of Π′_{j} and Π′′, for j ⪯ 1.

4.7 Lemma Application

Suppose we want to apply the sequent A_{0} ⋯ A_{m} (m ∈ N) as a lemma. Note that this will only be an equivalence transformation relative to the validity of the lemma. We present here a version with maximal downfolding (as used in QuodLibet, e.g.). Every level of user-controlled downfolding is obviously no problem.

↓ \frac{Π}{\overline{A_{0}} Π \overline{A_{1}} A_{0} Π ⋯ \overline{A_{m}} A_{m−1} … A_{0} Π}

↑ id ↑ \frac{(A′′_{0}∧ … ∧A′′_{m′}) Π′′}{Ξ′_{0} Π′_{0} ⋯ Ξ′_{m′} Π′_{m′}}

where the numbers of formulas of each of Π, Π′_{0}, …, Π′_{m′}, Π′′ are the same, where Π′′ is the intersection of Π′_{0}, …, Π′_{m′}, and where A′′_{j} is the formula of the sequent resulting from appending A′_{j}, Ξ′_{j}, and the difference of Π′_{j} and Π′′, for j ⪯ m′.

5 Examples

5.1 The Example of [3]

Let us replay the example of [3] here. We use automatic α-decomposition of not focused formulas. We start with the one formula sequent

¬((A ∧ B) ∨ (A ⇒ B)) ⇒ ¬((B ∨ C) ⇒ (A ∨ C))

Clicking to the ∧ we get (A ∧ B), ¬A, B, ¬((B ∨ C) ⇒ (A ∨ C)) A user might prefer a representation of the form

Focused: (A ∧ B) Rewrite Rules: A = true, B = false, …

No matter how it is presented to the user, by the automatic simplification part of unconditional contextual rewriting we immediately get

(A ∧ false), ¬A, B, ¬((B ∨ C) ⇒ (A ∨ C))

which is immediately simplified by automatic simplification into

false , ¬A, B, ¬((B ∨ C) ⇒ (A ∨ C))

Removing the single set pointer (focus) we get

¬(false ∨ (A ⇒ B)) ⇒ ¬((B ∨ C) ⇒ (A ∨ C))

which is immediately simplified to ¬(A ⇒ B) ⇒ ¬((B ∨ C) ⇒ (A ∨ C)) Next we focus on the last implication ¬A, B, ¬((B ∨ C) ⇒ (A ∨ C)) and automatic simplification immediately produces ¬A, B, false Removing the single set pointer (focus) we get ¬(A ⇒ B) ⇒ false which is automatically simplified to A ⇒ B

This series of equivalence transformations closely follows that of the example of [3] with exactly the same result. The slight differences improve the userfriendliness, namely that the focused formula does not jump out of its position and is always presented with positive polarity (the ‘¬’ does not disappear with the focus on ‘⇒’ above).

Moreover, in our case here, we have an additional possibility, namely not to remove the the first pointer before setting the second one. This results in

false , ¬A, B, ¬((B ∨ C) ⇒ (A ∨ C))

and then in  false , ¬A, B, false

This seems more natural because the basic idea of the whole transformation is to use ¬A and B for rewriting everywhere.

5.2 First-Order Example

Suppose we want to prove ∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)} ⇒ ∃x. ∀y. Q(x, y)

When the user clicks on the last Q he gets:

¬∀v. \binom{∀u. \underline{Q(u, v)}}{∨ ∀w. \underline{Q(v, w)}}, ∃x. ∀y. Q(x, y), Q(x0^{γ}, y0^{δ})

with the variable-condition \xymatrix{x0^{γ} \ar[r]_{R} & y0^{δ}} . Note that the two occurrences of Q

that are of complementary polarity to the Q in the focus should be highlighted by the system. We have underlined them here. So suppose the user clicks the first one. He gets:

¬∀u. \underline{Q(u, v0^{γ})}, ¬ Q(u0^{γ}, v0^{γ}) ,

¬∀v. \binom{∀u. \underline{Q(u, v)}}{∨ ∀w. \underline{Q(v, w)}}, ∃x. ∀y. \underline{Q(x, y)}, Q(x0^{γ}, y0^{δ})

Note that the system does not apply any unification right in the moment because v0^{γ} occurs also in another sequent, namely in

¬∀w. \underline{Q(v0^{γ}, w)}, ¬∀v. \binom{∀u. \underline{Q(u, v)}}{∨ ∀w. \underline{Q(v, w)}}, ∃x. ∀y. Q(x, y), Q(x0^{γ}, y0^{δ})

Nevertheless, the user cannot do anything anymore because the last sequentrewriting rule of automatic simplification (cf. Section 3) triggers automatic γdecomposition of the last formula, removing this branch. Then—the v0^{γ} now occurring only in one sequent—the system unifies the two focuses and replies with true, which the user only sees when the proof is done. Note that, although this proof looks very simple because it took only two quite arbitrary clicks by the user, the theorem is already quite hard to prove in natural deduction because it is not intuitionistically valid.

Acknowledgments: I am indebted to Serge Autexier who got me down the trees.

References

[1] Serge Autexier (2002). Theory and Architecture of an Hierarchical Contextual Reasoning Framework. Ph.D. thesis. To appear.

[2] Ulrich Kühler (2000). A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations. Ph.D. thesis, Infix, Sankt Augustin.

[3] Leonard G. Monk (1988). Inference Rules Using Local Contexts. J. Automated Reasoning 4, pp. 445–462, Kluwer.

[4] Peter J. Robinson, John Staples (1993). Formalizing a Hierarchical Structure of Practical Mathematical Reasoning. J. Logic Computat. 3, pp. 47–61, Oxford Univ. Press.

[5] Lincoln A. Wallen (1990). Automated Proof Search in Non-Classical Logics. MIT

Press. Cf., however, http://www.ags.uni-sb.de/˜ cp/p/wallen/all.txt for some

obsolete aspects of this fascinating book.

[6] Claus-Peter Wirth (1997). Positive/Negative-Conditional Equations: A Constructor-Based Framework for Specification and Inductive Theorem Proving. Ph.D. thesis, Verlag Dr. Kovač, Hamburg.

[7] Claus-Peter Wirth (2000). Descente Infinie + Deduction. Report 737/2000, FB Informatik, Univ. Dortmund. Extd. version, Dec. 13, 2002. http://www.ags.

uni-sb.de/˜ cp/p/tab99/new.html (Feb.01,2002).

5.3 Conditional Rewriting?

Let D[C] denote a huge formula in that C has a single positive occurrence. Consider ¬(A ⇒ (B ⇒ C)), D[C] In the system of [1] it is possible to use conditional rewriting with implications to rewrite C to to (A ∧ B), yielding something like

D[(A ∧ B)], ¬(A ⇒ (B ⇒ C)), D[C]

We could do this step only in case of the original sequent having the equivalent form ¬((A ∧ B) ⇒ C), D[C] These things seem wondrous.

5.4 Rewriting with β-blocks

Let C and D be formulas. Assume that the formula B is listed in the sequent Γ Π. Let A[D] denote the formula A[C] with some occurrences of C replaced with D. Now we can apply the rule

↓ \frac{Γ A[C] Π}{Γ A[D] A[C] Π} ↑ \frac{Ξ′ (A′_{0}∨A′_{1}) Π′}{Ξ′ A′_{0} A′_{1} Π′}

in any of the following cases:

1. B is a β-block for {C^{−}, D^{+}} and all occurrences of C in A[C] have positive polarity.

2. B is a β-block for {C^{+}, D^{−}} and all occurrences of C in A[C] have negative polarity.

β-blocks are inductively defined as follows: ¬(D⇒C), ¬(C⇐D), (D∧ \overline{C}), ( \overline{C} ∧D) ¬( \overline{D} ∨C) and ¬(C∨ \overline{D}), are β-blocks for C^{−} and D^{+}.

Every formula A can be seen as the singleton β-set {A^{+}}.

Then we may rewrite elements of β-sets as follows to several new elements as follows:

\begin{aligned}(A_{0}∧ … ∧A_{n+1})^{+} & → & A_{0}^{+}, …, A_{n+1}^{+} \\ (A_{0}∨ … ∨A_{n+1})^{−} & → & A_{0}^{−}, …, A_{n+1}^{−} \\ (A⇒B)^{−} & → & A^{+}, B^{−} \\ (A⇐B)^{−} & → & A^{−}, B^{+} \\ (¬A)^{−} & → & A^{+} \\ (¬A)^{+} & → & A^{−} \end{aligned}

Now B is a β-block for the β-set M if {B^{+}} and M rewrite to the same set. Actually, when rewriting {B^{+}} (but not for M), we additionally may allow the following steps here:

\begin{aligned}(A_{0}∧ … ∧A_{n+1})^{−} & → & (A_{0}∧ … ∧A_{i−1}∧A_{i+1}∧ … ∧A_{n+1})^{−} \\ (A_{0}∨ … ∨A_{n+1})^{+} & → & (A_{0}∨ … ∨A_{i−1}∨A_{i+1}∨ … ∨A_{n+1})^{+} \\ (A⇒B)^{+} & → & A^{−} \\ (A⇒B)^{+} & → & B^{+} \\ (A⇐B)^{+} & → & A^{+} \\ (A⇐B)^{+} & → & B^{−} \end{aligned}