% % Prover9 commands % op(400, infix, [^,v,"=>",*]). op(200, prefix, ~). lex([0, 1, *, ^, =>, v, ~]). assign(order,kbo). set(lex_order_vars). set(para_units_only). clear(back_demod). set(para_from_small). set(para_into_vars). set(restrict_denials). % % Input formulas % formulas(assumptions). % % Identities axiomatising Nelson FL_ew-algebras. % % Bounded lattice part (x v y) v z = x v (y v z) #label("(D1)"). (x ^ y) ^ z = x ^ (y ^ z) #label("(D2)"). x ^ x = x #label("(D3)"). x v x = x #label("(D4)"). x v y = y v x #label("(D5)"). x ^ y = y ^ x #label("(D6)"). x v (x ^ y) = x #label("(D7)"). x ^ (x v y) = x #label("(D8)"). x ^ 0 = 0 #label("(D9)"). x ^ 1 = x #label("(D10)"). % Monoid part x * 1 = x #label("(M1)"). x * y = y * x #label("(M2)"). (x * y) * z = x * (y * z) #label("(M3)"). % Residuation part x * (y v z) = (x * y) v (x * z) #label("(R1)"). x => (y ^ z) = (x => y) ^ (x => z) #label("(R2)"). (x * (x => y)) v y = y #label("(R3)"). (x => (x * y)) ^ y = y #label("(R4)"). % Nelson part x => (x => (x => y)) = x => (x => y) #label("(E_2)"). % 3-potency (x v y) ^ (x v z) = x v (y ^ z) #label("(D11)"). % Distributivity (x ^ y) v (x ^ z) = x ^ (y v z) #label("(D12)"). ~(~x) = x #label("(I)"). % Involution (x => (x => y)) ^ (~y => (~y => ~x)) = x => y #label("(N)"). % Nelson identity % % Definitions mapping Nelson FL_ew-algebras to Alg Mod* F**-algebras % % Definition of ~ (negation operation) in Nelson FL_ew-algebras ~x = x => 0 #label("(~ def)"). end_of_list. formulas(goals). % % Identities and quasi-identities axiomatising Alg Mod* F**. % all x all y (((x = 1) & (x => y = 1)) -> (y = 1)) #label("(3)"). end_of_list. % % Hints extracted from previously found proofs. % formulas(hints). x = 1 ^ x. 1 ^ x = x. x * (c1 => c2) = x. 1 v x = 1. c1 v x = 1. c1 v c2 = c2. c2 = 1. end_of_list.