% % Prover9 commands % clear(auto). op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). lex([0,1,*,^,=>,->,v,~,-]). assign(order,kbo). set(lex_order_vars). set(paramodulation). set(para_units_only). clear(back_demod). set(hyper_resolution). set(auto_denials). set(restrict_denials). % ************************************************************************** % Clauses for Section 4 % ************************************************************************** formulas(assumptions). % % Identities axiomatising lattices % (x v y) v z = x v (y v z) # label("(D1)"). (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). x v y = y v x # label("(D3)"). x ^ y = y ^ x # label("(D4)"). x v (x ^ y) = x # label("(D5)"). x ^ (x v y) = x # label("(D6)"). % % Identities and quasi-identities axiomatising BCK-algebras % (x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)"). 1 => x = x # label("(BCK2)"). x => 1 = 1 # label("(BCK3)"). x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). % % Identities axiomatising partially ordered, commutative integral % residuated monoids (pocrims) % % Note: These identities axiomatise pocrims when taken in % conjunction with the identities and quasi-identities axiomatising % BCK-algebras given above. % x * 1 = x # label("(M1)"). x * y = y * x # label("(M2)"). (x * y) * z = x * (y * z) # label("(M3)"). (x * y) => z = x => (y => z) # label("(P)"). % % Identities axiomatising commutative, integral residuated lattices % % Note: These identities axiomatise commutative, integral residuated % lattices when taken in conjunction with the identities and % quasi-identities axiomatising pocrims given above. % % Note: This quasi-equational basis for commutative, integral % residuated lattices axiomatises them as structures % , 1> with a lattice reduct , % a pocrim reduct , 1>, such that (i) 1 is the greatest % element with respect to the lattice partial ordering; and % (ii) the lattice partial order and BCK-algebra partial orders % coincide. % x ^ 1 = x # label("(D10)"). x ^ ((x => y) => y) = x # label("(3.7)"). (x ^ y) => y = 1 # label("(3.11)"). % % Identities axiomatising FL_ew-algebras % % Note: These identities axiomatise FL_ew-algebras % when taken in conjunction with the identities and % quasi-identities axiomatising commutative, integral % residuated lattices given above. % x v 0 = x # label("(D9)"). % % Definitions mapping Nelson FL_ew-algebras to Nelson algebras % % Definition of -> (weak implication) in Nelson FL_ew-algebras x -> y = x => (x => y) # label("(-> def)"). % Definition of ~ (strong negation) in Nelson FL_ew-algebras. ~x = x => 0 # label("(~ def)"). % Definition of - (weak negation) in Nelson FL_ew-algebras -x = x => (x => 0) # label("(- def)"). % % Identities axiomatising Nelson FL_ew-algebras. % % Note: Nelson FL_algebras are 3-potent, distributive classical % FL_ew-algebras satisfying the Nelson identity (N). % % Note: The identities expressing classicality and the Nelson identity % are expressed in terms of the definitions mapping Nelson FL_ew-algebras % into Nelson algebras. % x => (x => (x => y)) = x => (x => y) # label("(E_2)"). % 3-potency (x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). % Distributivity (x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)"). ~(~x) = x # label("(DN)"). % Classicality (x -> y) ^ (~y -> ~x) = x => y # label("(N)"). % Nelson identity % % Identities which are known consequences of the theory of FL_ew-algebras % % Note: The following identities are known to hold for BCK-algebras, and % hence hold for Nelson FL_ew-algebras. % (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). x => ((x => y) => y) = 1 # label("(BCK5)"). x => x = 1 # label("(3.16)"). x => (y => x) = 1 # label("(3.17)"). x => (y => z) = y => (x => z) # label("(3.18)"). % % Note: The following identities are known to hold for commutative, % integral residuated lattices, and hence hold for Nelson FL_ew-algebras. % (x * y) v (x * z) = x * (y v z) # label("(4.1)"). (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). (x * (x => y)) v y = y # label("(4.3)"). (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). end_of_list. % % Previous results % formulas(assumptions). % Lemma 4.3 (x => y) ^ y = y # label("(3.13)"). % Lemma 4.3 (1) (x v y) => y = x => y # label("(4.6)"). % Lemma 4.3 (2) x -> (y => z) = y => (x -> z) # label("(4.7)"). % Lemma 4.3 (3) x ^ (~x => y) = x # label("(4.8)"). % Lemma 4.3 (4) % Lemma 4.4 x -> ((y v x) -> z) = x -> z # label("(4.9)"). % Lemma 4.4 (1) x -> (~x v y) = x -> y # label("(4.10)"). % Lemma 4.4 (2) x -> x = 1 # label("(N2)"). % Lemma 4.5 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). % Lemma 4.6 end_of_list. % % Current problem (Lemma 4.7) % formulas(goals). (x -> y) ^ (~x v y) = ~x v y # label("(N3)"). % Lemma 4.7 end_of_list. % % Hints extracted from previously found proofs. % formulas(hints). (x * x) => y = x -> y. (x -> y) ^ y = y. end_of_list.