logic/logic_b.in


1
2
3
4
5
6
7
8
9
10
11
12

formulas(sos).
	(x*(y*z)=(x*y)*z).
	(x*I=x).
	(x*inv(x)=I).
end_of_list.

formulas(goals).
	all x (I*x=x).
	all x (inv(inv(x))=x).
	all x (inv(x)*x=I).
	all x all y (x*y=y*x).
end_of_list.