% problem-set/algebra/boolean/prob2_part1.ver2
% created: 07/31/89
% revised: 08/02/89

% description:
%
% This problem is designed to prove that x + x = x in boolean
% algebra.  

% This version uses equality representation and demodulators.
% Paramodulation is the inference rule, and para_from_left is set.

% representation:
%
% prod(a,b) = c  means a * b = c.
% sum(a,b) = c  means a + b = c.
%
% declare_functions(2,[sum, prod]).
% declare_function(1,comp).
% declare_variables([x,y,z,u,v,v1,v2,v3,v4]).
% declare_constants([0,1,a]).

set(dynamic_demod).
set(para_from).
set(para_into).
%set(para_from_right).
set(para_from_left).
assign(max_seconds,40).

list(axioms). 

% reflexivity
(x = x).

% commutativity
(sum(x,y) = sum(y,x)).
(prod(x,y) = prod(y,x)).

% distributivity
(sum(prod(x,y), z) = prod(sum(x,z), sum(y,z))).
(sum(x, prod(y,z)) = prod(sum(x,y), sum(x,z))).
(prod(sum(x,y), z) = sum(prod(x,z), prod(y,z))).
(prod(x, sum(y,z)) = sum(prod(x,y), prod(x,z))).

end_of_list.

 
list(sos). 

% existence of complements
(sum(x, comp(x)) = 1).
(sum(comp(x), x) = 1).
(prod(x, comp(x)) = 0).
(prod(comp(x), x) = 0).

% existence of identities
(sum(x,0) = x).
(sum(0,x) = x).
(prod(x,1) = x).
(prod(1,x) = x).

% denial of the theorem 

-(sum(a,a) = a).

end_of_list.

list(demodulators).

% commutativity
(sum(x,y) = sum(y,x)).
(prod(x,y) = prod(y,x)).

% distributivity
(sum(prod(x,y), z) = prod(sum(x,z), sum(y,z))).
(sum(z, prod(x,y)) = prod(sum(z,x), sum(z,y))).

% existence of complements
(sum(x, comp(x)) = 1).
(sum(comp(x), x) = 1).
(prod(x, comp(x)) = 0).
(prod(comp(x), x) = 0).

% existence of identities
(sum(x,0) = x).
(sum(0,x) = x).
(prod(x,1) = x).
(prod(1,x) = x).

end_of_list.

