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
tis 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.
% 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.
| 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 | (KA1) | |
| KpAqr <- AKpqKpr | (KA2) |
| ApKqr -> KApqApr | (AK1) | |
| ApKqr <- KApqApr | (AK2) |
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) CNCCNCCpqqNCCprrNCCprrCCpNCCNqNrNrNCCNqNrNrwhich 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.
For more information on the Harris/Fitelson work on distributivity presented in [3], see the paper's companion Web page.
% 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.
These results are relevant to a larger work ([2]) concerning the elimination of occurrences of double negation in proofs.
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.
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.outprooftrans -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.
% 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
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.
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
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.
[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)