Posted on the Web June 6, 2001. Last updated on May 8, 2011 by Bob Veroff.

# Challenge Problems with Condensed Detachment

This page (still under development) will summarize our most recent work with logical systems based on the inference rule condensed detachment (CD):
```   i(s,t)   (major premise)
r        (minor premise)
------------------------
sigma(t), where sigma is a most general unifier for terms r and s.
```
In particular, we focus here on proving theorems in these logical calculi using resolution-style automated reasoning programs such as Otter [4]. The questions considered include determining the equivalence of various axiom systems, finding proofs to specific theorems, and finding proofs with certain specified properties.

CD problems are easily represented for resolution theorem provers. If we let

`     P(t)`
represent the assertion that
`     t`
is a theorem, then applications of condensed detachment can be implemented using hyperresolution and the following clause.
```     -P(i(x,y)) | -P(x) | P(y).

```
The page currently includes the following.

### 1. Distributivity Theorems in Many-Valued Logic

Many-valued logic (MV) can be described, in clause form, with the following four axioms.
```   % axioms for many-valued logic
P(i(x,i(y,x)))                         (MV1)
P(i(i(x,y),i(i(y,z),i(x,z))))          (MV2)
P(i(i(i(x,y),y),i(i(y,x),x)))          (MV3)
P(i(i(n(x),n(y)),i(y,x)))              (MV4)
```
The problem is to find CD-only proofs of the following four distributivity theorems.
```   % KA1: K distributes over A, direction 1 (KpAqr -> AKpqKpr)
P(i(n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z)))),
i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(n(x),n(z)),n(z)))),n(i(i(n(x),n(z)),n(z)))))) # label("KA1").

% KA2: K distributes over A, direction 2 (KpAqr <- AKpqKpr)
P(i(i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(n(x),n(z)),n(z)))),n(i(i(n(x),n(z)),n(z)))),
n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z)))))) # label("KA2").

% AK1: A distributes over K, direction 1 (ApKqr -> KApqApr)
P(i(i(i(x,n(i(i(n(y),n(z)),n(z)))),n(i(i(n(y),n(z)),n(z)))),
n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))))) # label("AK1").

% AK2: A distributes over K, direction 2 (ApKqr <- KApqApr)
P(i(n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))),
i(i(x,n(i(i(n(y),n(z)),n(z)))),n(i(i(n(y),n(z)),n(z)))))) # label("AK2").
```
The comments refer to operators A and K, which are defined below.

Previous proofs of these theorems rely on several lemmas and on meta-theoretical inferences such as term-level equality substitutions ([1]). Our interest is in using an automated reasoning program such as Otter to find proofs that rely solely on the axioms and on applications of condensed detachment. In particular, the challenge is to find these proofs from scratch--without relying on any knowledge of the known meta-theoretical proofs. Our approach is to find meta-theoretical proofs of our own, which are in turn used as proof sketches ([8]) to help Otter find the desired CD-only proofs.

#### Background

In the notation of [6] and [1], the axioms for MV are stated as

 CpCqp (MV1) CCpqCCqrCpr (MV2) CCCpqqCCqpp (MV3) CCNpNqCqp (MV4)

where C and N are related, respectively, to our usual notions of logical implication and negation. In addition, two operators A and K are defined as follows.

 Apq = CCpqq Kpq = NCCNpNqNq

These two operators are related, respectively, to our usual notions of logical disjunction (or) and conjunction (and).

It is known that the following distributivity properties hold for K and A.

 KpAqr = AKpqKpr (K distributes over A) ApKqr = KApqApr (A distributes over K)

In the primitives of MV, these are stated as four implications:

• KpAqr = AKpqKpr       (K distributes over A)

 KpAqr -> AKpqKpr (KA1) KpAqr <- AKpqKpr (KA2)

• ApKqr = KApqApr       (A distributes over K)

 ApKqr -> KApqApr (AK1) ApKqr <- KApqApr (AK2)

where -> denotes an application of C.

Expanding the four theorems with the definitions of A and K gives

```   % KA1: K distributes over A, direction 1 (KpAqr -> AKpqKpr)
CNCCNpNCCqrrNCCqrrCCNCCNpNqNqNCCNpNrNrNCCNpNrNr

% KA2: K distributes over A, direction 2 (KpAqr <- AKpqKpr)
CCCNCCNpNqNqNCCNpNrNrNCCNpNrNrNCCNpNCCqrrNCCqrr

% AK1: A distributes over K, direction 1 (ApKqr -> KApqApr)
CCCpNCCNqNrNrNCCNqNrNrNCCNCCpqqNCCprrNCCprr

% AK2: A distributes over K, direction 2 (ApKqr <- KApqApr)
CNCCNCCpqqNCCprrNCCprrCCpNCCNqNrNrNCCNqNrNr
```
which correspond directly to the clauses presented at the beginning of this section. In clause form, Cpq is represented as i(p,q); Np is represented as n(p); and the propositional variables p, q, and r are represented, respectively, with the Otter variables x, y, and z.

#### Proofs

Here are our Otter proofs of the four theorems.
We note that a CD-only proof of KA1 appears in [3]. Proofs for AK1 and AK2 are mentioned in that same paper (footnote #8), but no proofs are provided, and we believe that the mentioned proofs are hybrid equality/CD proofs. As far as we know, the proofs presented here for KA2, AK1, and AK2 are the first explicitly presented CD-only proofs.

For more information on the Harris/Fitelson work on distributivity presented in [3], see the paper's companion Web page.

#### Acknowledgements

Branden Fitelson and Larry Wos introduced me to these problems and directed me to the relevant background information.

### 2. Finding CD-Derivations of Specific Instances

The problem is to find CD-only derivations of
```   % theorem d2
P(i(i(x,x),i(n(x),n(x)))).

% theorem d3
P(i(i(x,x),i(i(y,y),i(i(x,y),i(x,y))))).
```
in many-valued logic (MV)
```   % axioms for many-valued logic
P(i(x,i(y,x)))                         (MV1)
P(i(i(x,y),i(i(y,z),i(x,z))))          (MV2)
P(i(i(i(x,y),y),i(i(y,x),x)))          (MV3)
P(i(i(n(x),n(y)),i(y,x)))              (MV4)
```
and also in the intuitionistic logic (H)
```   % axioms for intuitionistc logic
P(i(x,i(y,x)))                         (H1)
P(i(i(x,i(y,z)),i(i(x,y),i(x,z))))     (H2)
P(i(i(x,n(x)),n(x)))                   (H3)
P(i(x,i(n(x),y)))                      (H4)
```
These theorems are instances of more general theorems that are not difficult to prove. What makes these problems interesting (and challenging) is the requirement of deriving precisely the specified instances of the theorems.

#### Proofs

Here are our Otter proofs (derivations) of the four theorems.
We note that all four proofs are double negation free. That is, no step contains a term of the form n(n(t)), where t is a term.

These results are relevant to a larger work ([2]) concerning the elimination of occurrences of double negation in proofs.

#### Acknowledgements

Michael Beeson and Larry Wos introduced me to these problems.

### 3. Proving the Harris / Rezus Single Axiom is a Theorem in Many-Valued Logic

The Harris / Rezus axiom,

```   P(i(i(i(x,i(y,x)),i(i(i(i(i(i(i(i(i(z,u),i(i(v,z),i(v,u))),i(i(w,i(v6,w)),v7)),v7),i(i(i(i(v8,v9),v9),i(i(v9,v8),v8)),v10)),v10),i(i(i(i(v11,v12),i(v12,v11)),i(v12,v11)),v13)),v13),i(i(v14,i(v15,v14)),v16))),v16)).
```
is known to be a single axiom for the implicational fragment of many-valued logic, which can be described in clause form with the following four axioms.
```   % axioms for the implicational fragment of many-valued logic
P(i(x,i(y,x)))                         (MV1)
P(i(i(x,y),i(i(y,z),i(x,z))))          (MV2)
P(i(i(i(x,y),y),i(i(y,x),x)))          (MV3)
P(i(i(i(x,y),i(y,x)),i(y,x)))          (MV5)
```
The problem here is to find a CD-only derivation of the Harris / Rezus axiom from this set of axioms. The problem is challenging because of the length of the formula to be proved.

As far as we know, this is the first explicitly presented CD-only proof.

#### Background

According to Ken Harris, the Harris / Rezus axiom was produced by applying a method due to Adrian Rezus ([5]), which in turn was based on work by Alfred Tarski. The relevant Tarski work, which was done in the 1920s, can be found in [7].

### 4. CD-Derivation of the Long Rezus Single Axiom for RI from {B,C,I,W}

From

```   P(i(i(u,v),i(i(v,w),i(u,w))))     (B)
P(i(i(u,i(v,w)),i(v,i(u,w))))     (C)
P(i(u,u))                         (I)
P(i(i(u,i(u,v)),i(u,v)))          (W)
```
derive
```   % A Rezus-style single axiom for RI
P(i(i(i(x,i(i(i(y,y),i(i(z,z),i(i(u,u),i(i(v,v),i(x,w))))),w)),i(i(i(i(i(v6,v7),i(i(v7,v8),i(v6,v8))),i(i(i(i(i(v9,i(v9,v10)),i(v9,v10)),i(i(i(v11,v12),i(i(v12,v13),i(v11,v13))),v14)),v14),v15)),v15),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)).
```
We include input, output, proof and xml files created as follows.
prover9 -f RI_rezus.in > RI_rezus.out

prooftrans -f RI_rezus.out > RI_rezus.pf

prooftrans xml -f RI_rezus.out > RI_rezus.xml

We note that this essentially is a proof checking run, since it includes the steps from a previously found proof as hints. The original proofs were found using the method of proof sketches ([8]). In particular, our approach was to find derivations of the Rezus axiom with extra assumptions included as input; the resulting derivations in turn were used as proof sketches to help Prover9 find the desired CD-only proofs.

### 5. Whitehead and Russell Dependency

From
```   % Definition:  x -> y = ~x v y
P((x -> y) -> (~x v y))                (-> Definition, part a)
P((~x v y) -> (x -> y))                (-> Definition, part b)

% WR axioms WR1 .. WR4
P((x v x) -> x)                        (WR1)
P(y -> (x v y))                        (WR2)
P((x v y) -> (y v x))                  (WR3)
P((y -> z) -> ((x v y) -> (x v z)))    (WR4)
```
derive
```   P((x v (y v z)) -> (y v (x v z)))      (WR5)
```
This establishes the dependency of WR5 in Whitehead and Russell's system for PC.

We include input, output, proof and xml files created as follows.

prover9 -f WandR.in > WandR.out

prooftrans -f WandR.out > WandR.pf

prooftrans xml -f WandR.out > WandR.xml

We note that this essentially is a proof checking run, since it includes the steps from a previously found proof as hints. The original proofs were found using the method of proof sketches ([8]). In particular, our approach was to find derivations of WR5 with extra assumptions included as input; the resulting derivations in turn were used as proof sketches to help Prover9 find the desired CD-only proofs.

### 6. Theorems in Intuitionistic Logic

See AAR Newsletter #91 (April 2011).

From

```   P(i(x,i(y,x)))                        (A1)
P(i(i(x,i(y,z)),i(i(x,y),i(x,z))))    (A2)
P(i(k(x,y),x))                        (A3)
P(i(k(x,y),y))                        (A4)
P(i(i(x,y),i(i(x,z),i(x,k(y,z)))))    (A5)
P(i(x,a(x,y)))                        (A6)
P(i(x,a(y,x)))                        (A7)
P(i(i(x,y),i(i(z,y),i(a(x,z),y))))    (A8)
P(i(i(x,n(y)),i(y,n(x))))             (A9)
P(i(n(x),i(x,y)))                     (A10)
```
derive
```   P(i(i(x,y),i(a(x,z),a(y,z))))                                           (H334)
P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(x,z),a(y,z)),a(k(x,y),z))))   (HIF4)
P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(x),n(y)),n(a(x,y)))))               (HIF5)
```

We include input, output, proof and xml files created as follows.

prover9 -f IL.in > IL.out

prooftrans -f IL.out > IL.pf

prooftrans xml -f IL.out > IL.xml

We note that this essentially is a proof checking run, since it includes the steps from a previously found proof as hints. The original proofs were found using the method of proof sketches ([8]). In particular, our approach was to find derivations with extra assumptions included as input; the resulting derivations in turn were used as proof sketches to help Prover9 find the desired CD-only proofs.

### References

[1] Beavers, G., ``Distribution in Lukasiewicz logics,'' Bulletin of the Section of Logic, vol 21, no. 4, pp. 140-146 (1992). (pdf)

[2] Beeson, M., Veroff, R., and Wos, L., ``Double negation elimination in some propositional logics,'' Studia Logica, 80:195-234, 2005. (pdf)

[3] Harris, K. and Fitelson, B., ``Distributivity in L_aleph0 and other sentential logics,'' Journal of Automated Reasoning, Vol. 27, no. 2, pp. 141-156 (2001). (pdf)

[4] McCune, W., OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois, 1994.

[5] Rezus, A., ``On a theorem of Tarski,'' Libertas Mathematica, vol 2, pp. 63-97 (1982).

[6] Rose, A. and Rosser, J., ``Fragments of many-valued statement calculi,'' Trans. American Mathematical Society, vol 87, pp. 1-53 (1958).

[7] Tarski, A., ``Investigations into the sentential calculus,'' in Logic, Semantics and Metamathematics, Hackett Publishing, Indianapolis (1983).

[8] Veroff, R., ``Solving open questions and other challenge problems using proof sketches,'' Journal of Automated Reasoning, Vol. 27, no. 2, pp. 157-174 (2001). (postscript)