Matthew Spinks and Robert Veroff
September 2009
This page provides Web support for
Slaney's Logic F** is Constructive Logic with Strong Negation [3].In particular, we present here proofs that were found with the assistance of the program Prover9 [1].
For each proof, we include input, output, proof and xml files created as follows.
prover9 -f file.in > file.outprooftrans -f file.out > file.pf
prooftrans xml -f file.out > file.xml
We note that these essentially are proof-checking runs, since they include steps from previously found proofs as hints. The original proofs were found using the method of proof sketches [5]. 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 proofs.
% % Identities and quasi-identities axiomatising Alg Mod* F**. % x => ((x => y) => y) = 1 (A1)[= 1] (x => y) => ((y => z) => (x => z)) = 1 (A2)[= 1] (x ^ y) => x = 1 (A3)[= 1] (x ^ y) => y = 1 (A4)[= 1] ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1 (A5)[= 1] x => (x v y) = 1 (A6)[= 1] y => (x v y) = 1 (A7)[= 1] ((x => z) ^ (y => z)) => ((x v y) => z) = 1 (A8)[= 1] (x ^ (y v z)) => ((x ^ y) v z) = 1 (A9)[= 1] ~x => x = 1 (A10)[= 1] (x => ~y) => (y => ~x) = 1 (A11)[= 1] x => (y => x) = 1 (A12)[= 1] ((x => (x => y)) ^ (~y => (x => y))) => (x => y) = 1 (A13)[= 1] all x all y (((x = 1) & (x => y = 1)) -> (y = 1)) (3) all x all y (((x = 1) & (y = 1)) -> (x ^ y = 1)) (4) all x all y (((x => y = 1) & (y => x = 1)) -> (x = y)) (5)Proof of (A1)-(A13). (in, out, pf, xml)
Proof of (3). (in, out, pf, xml)
Proof of (4). (in, out, pf, xml)
Proof of (5). (in, out, pf, xml)
x => x = y => y (7) ~x = x => ~(y => y) (8) x => y = ~y => ~x (9)Proof. (in, out, pf, xml)
% % Identities axiomatising Nelson FL_ew-algebras. % % Bounded lattice part (x v y) v z = x v (y v z) (D1) (x ^ y) ^ z = x ^ (y ^ z) (D2) x ^ x = x (D3) x v x = x (D4) x v y = y v x (D5) x ^ y = y ^ x (D6) x v (x ^ y) = x (D7) x ^ (x v y) = x (D8) x ^ 0 = 0 (D9) x ^ 1 = x (D10) % Monoid part x * 1 = x (M1) x * y = y * x (M2) (x * y) * z = x * (y * z) (M3) % Residuation part x * (y v z) = (x * y) v (x * z) (R1) x => (y ^ z) = (x => y) ^ (x => z) (R2) (x * (x => y)) v y = y (R3) (x => (x * y)) ^ y = y (R4) % Nelson part x => (x => (x => y)) = x => (x => y) (E_2, 3-potency) (x v y) ^ (x v z) = x v (y ^ z) (D11) (x ^ y) v (x ^ z) = x ^ (y v z) (D12) ~(~x) = x (I) (x => (x => y)) ^ (~y => (~y => ~x)) = x => y (N, Nelson identity)Proof. (in, out, pf, xml)