% problem-set/algebra/boolean/prob8.ver1
% created: 07/09/86
% revised: 07/27/89

% description:
% 
% This problem is designed to prove that -(-x) = x
% in boolean algebra.  This version is from the 
% McCharen paper [Aug 1976].

% A weighting scheme was used.

% representation:
% 
% PROD(a,b,c) means a * b = c.
% SUM(a,b,c) means a + b = c.
%
% declare_predicates(3,[SUM,PROD]).
% declare_predicate(2,EQUAL).
% declare_functions(2,[f1,f2]).
% declare_function(1,comp).
% declare_variables([x,y,z,u,v,v1,v2,v3,v4]).
% declare_constants([0,1,a]).

set(factor).
set(hyper_res).
assign(max_seconds,100). 

list(axioms).

%  commutative property 

-SUM(x,y,v3)  |  SUM(y,x,v3).
-PROD(x,y,v3) |  PROD(y,x,v3).

%  distributive property 

-PROD(x,y,v1)  | -PROD(x,z,v2)  | -SUM(y,z,v3)  | -PROD(x,v3,v4)
| SUM(v1,v2,v4).
-PROD(x,y,v1)  | -PROD(x,z,v2)  | -SUM(y,z,v3)  | -SUM(v1,v2,v4)
| PROD(x,v3,v4).
-PROD(y,x,v1)  | -PROD(z,x,v2)  | -SUM(y,z,v3)  | -PROD(v3,x,v4)
| SUM(v1,v2,v4).
-PROD(y,x,v1)  | -PROD(z,x,v2)  | -SUM(y,z,v3)  | -SUM(v1,v2,v4)
| PROD(v3,x,v4).
-SUM(x,y,v1)   | -SUM(x,z,v2)   | -PROD(y,z,v3) | -SUM(x,v3,v4)
| PROD(v1,v2,v4).
-SUM(x,y,v1)   | -SUM(x,z,v2)   | -PROD(y,z,v3) | -PROD(v1,v2,v4)
| SUM(x,v3,v4).
-SUM(y,x,v1)   | -SUM(z,x,v2)   | -PROD(y,z,v3) | -SUM(v3,x,v4)
| PROD(v1,v2,v4).
-SUM(y,x,v1)   | -SUM(z,x,v2)   | -PROD(y,z,v3) | -PROD(v1,v2,v4)
| SUM(v3,x,v4).

%  existence of complements 

SUM(x,comp(x),1).
SUM(comp(x),x,1).
PROD(x,comp(x),0).
PROD(comp(x),x,0).

%  the above operations are well defined 

-SUM(x,y,u)    | -SUM(x,y,v)    | EQUAL(u,v).
-PROD(x,y,u)   | -PROD(x,y,v)   | EQUAL(u,v).

%  equality axioms 

EQUAL(x,x).
-EQUAL(x,y)    |  EQUAL(y,x).
-EQUAL(x,y)    | -EQUAL(y,z)    | EQUAL(x,z).

%  equality substitution axioms

-EQUAL(x,y)    | -SUM(x,v1,v2) | SUM(y,v1,v2).
-EQUAL(x,y)    | -SUM(v1,x,v2) | SUM(v1,y,v2).
-EQUAL(x,y)    | -SUM(v1,v2,x) | SUM(v1,v2,y).
-EQUAL(x,y)    | -PROD(x,v1,v2) | PROD(y,v1,v2).
-EQUAL(x,y)    | -PROD(v1,x,v2) | PROD(v1,y,v2).
-EQUAL(x,y)    | -PROD(v1,v2,x) | PROD(v1,v2,y).
-EQUAL(x,y)    |  EQUAL(f1(x,v1),f1(y,v1)).
-EQUAL(x,y)    |  EQUAL(f1(v1,x),f1(v1,y)).
-EQUAL(x,y)    |  EQUAL(f2(x,v1),f2(y,v1)).
-EQUAL(x,y)    |  EQUAL(f2(v1,x),f2(v1,y)).
-EQUAL(x,y)    |  EQUAL(comp(x),comp(y)).

end_of_list.

list(sos).

%  existence of identities 

SUM(x,0,x).
SUM(0,x,x).
PROD(x,1,x).
PROD(1,x,x).

%  closure property 

SUM(x,y,f1(x,y)).
PROD(x,y,f2(x,y)).

% denial of the theorem

-EQUAL(comp(comp(a)),a).

end_of_list.


weight_list(pick_given).
weight(f1(x,y), 4).
weight(f2(x,y), 2).
end_of_list.

