% % Prover9 commands % op(400,infix,[^,v,"=>",*]). clear(auto). set(hyper_resolution). % ************************************************************************** % Clauses for Section 5 (logic) (based on file clsn2.pdf dated 2008-29-06) % ************************************************************************** formulas(usable). % % Rule of inference (modus ponens) for FL_ew. % -P(x => y) | -P(x) | P(y) # label("MP"). end_of_list. formulas(assumptions). % % Theses axiomatising FLew. % % Note: These theses together with the rule of inference (MP) above % axiomatise the deductive system H of Section 5 of Part II. By Lemma 5.4 % of Part II, the deductive system H is FL_ew. % P((x => y) => ((y => z) => (x => z))) # label("(A1)"). P((x => (y => z)) => (y => (x => z))) # label("(A2)"). P(x => (y => x)) # label("(A3)"). P(x => (y => (x * y))) # label("(A4)"). P((x => (y => z)) => ((x * y) => z)) # label("(A5)"). P((x ^ y) => x) # label("(A6)"). P((x ^ y) => y) # label("(A7)"). P((x => y) => ((x => z) => (x => (y ^ z)))) # label("(A8)"). P(x => (x v y)) # label("(A9)"). P(y => (x v y)) # label("(A10)"). P((x => z) => ((y => z) => ((x v y) => z))) # label("(A11)"). P(1) # label("(A12)"). P(0 => x) # label("(A13)"). % Current problem (Lemma 5.1) P(A => B). P(B => A). P(C => D). P(D => C). -P((A ^ C) => (B ^ D)) | -P((A v C) => (B v D)). %-P((A ^ C) => (B ^ D)). %-P((A v C) => (B v D)). end_of_list. % % Hints extracted from previously found proofs. % formulas(hints). P((x => y) => ((y => z) => (x => z))). P((x ^ y) => x). P((x ^ y) => y). P((x => y) => ((x => z) => (x => (y ^ z)))). P(x => (x v y)). P(x => (y v x)). P((x => y) => ((z => y) => ((x v z) => y))). P(A => B). P(C => D). P((x => y) => ((x ^ z) => y)). P((x => y) => ((z ^ x) => y)). P((B => x) => (A => x)). P((D => x) => (C => x)). P(A => (B v x)). P((x => (B v y)) => ((A v x) => (B v y))). P(C => (x v D)). P((A ^ x) => B). P(((A ^ x) => y) => ((A ^ x) => (B ^ y))). P((x ^ C) => D). P((A v C) => (B v D)). P((A ^ C) => (B ^ D)). end_of_list.