% Language Options %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% op(500, infix, "\/"). op(500, infix, "/\"). op(300, postfix, "'"). op(450, infix, "*"). op(300, postfix, "^"). if(Prover9). % Options for Prover9 assign(max_seconds, 3000). end_if. if(Mace4). % Options for Mace4 assign(max_seconds, 3000). end_if. formulas(assumptions). % axioms of Boolean algebra %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %commutativity x \/ y = y \/ x. x /\ y = y /\ x. %associativity x \/ (y \/ z) = (x \/ y) \/ z. x /\ (y /\ z) = (x /\ y) /\ z. %absorption x \/ (y /\ x) = x. x /\ (y \/ x) = x. % ordering x <= y <-> x \/ y = y. x <= y <-> x /\ y = x. %distributivity x /\ (y \/ z) = (x /\ y) \/ (x /\ z). x \/ (y /\ z) = (x \/ y) /\ (x \/ z). %constants L = x \/ x'. O = x /\ x'. % composition %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% x * (y * z) = (x * y) * z. x * I = x. I * x = x. % Schroeder/Dedekind %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% x*y /\ z <= (x /\ z*y^) * (y /\ x^*z). x*y <= z <-> x^ * z' <= y'. x*y <= z <-> z' * y^ <= x'. % Tarski rule %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -(x = O) <-> (L*x)*L = L. %aux lemmas (proven before)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %to get a suitable set of axioms (x \/ y)*z = x*z \/ y*z. z*(x \/ y) = z*x \/ z*y. (x * y)^ = y^ * x^. (x \/ y)^ = x^ \/ y^. (x /\ y)^ = x^ /\ y^. x <= y -> x*z <= y*z. x <= y -> z*x <= z*y. x <= y -> x \/ z <= y \/ z. x <= y -> x /\ z <= y /\ z. x^^ = x. O <= x. x <= L. O*x = O. x*O = O. % predicate for points %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% point(x) <-> (x*L = x & L*x = L & x*x^ <= I). % predicates for specific relations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% irreflexive(x) <-> x <= I'. symmetric(x) <-> x = x^. univalent(x) <-> x^*x <= I. coloringProperty(x,z) <-> x*x^ <= z'. end_of_list. formulas(goals). % Lemma 3.2 - time 0m0.472s %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% all p all q (x*L != L & univalent(x) & point(p) & point(q) & p <= (x*L)' -> univalent(x \/ p*q^)). end_of_list.