/* Plaisted: ``Here's a problem where my prover is unusually slow with respect to Setheo. I'd be curious to know how your prover does, both with and without special equality reasoning. It takes Setheo a few seconds and our prover about 1000 or 2000 seconds I think.'' The problem is a specification of a non-commutative ring with unit, and we prove that (-x)*(-y) = x*y. This set of axioms is obtained by applying Brand's method to an equational specification of the same problem. Seems to show that it's much better to use functions + equality explicitly rather than what you would get with Brand's transformation. */ % plus is a *total* binary function (call it ``+'') plus(X,Y,+(X,Y)). plus(X, Y, U), plus(X, Y, V) -> U=V. % plus is AC % X+(Y+Z)=(X+Y)+Z. plus(X,Y,U), plus(Y,Z,V), plus(X,V,W) -> plus(U,Z,W). %plus(X,Y,U), plus(Y,Z,V), plus(U,Z,W) -> plus(X,V,W). % redundant % X+Y=Y+X. plus(Y, X, Z) == plus(X,Y,Z). % plus has an inverse (call it ``-'') plus(-(X), X, 0). % plus has a unit element (call it ``0'') plus(0, X, X). plus(X,0,X). % consequence plus(X,-(X),0). % not used; trivial consequence of the other axioms % mult is a binary function (call it ``*'') mult(X, Y, *(X, Y)). mult(X, Y, U), mult(X, Y, V) -> U=V. % mult is associative mult(X,Y,U), mult(Y,Z,V), mult(X,V,W) -> mult(U,Z,W). % mult has e left and right unit mult(0, X, 0). mult(X, 0, 0). % mult left-distributes over plus goal plus(Y,Z,V), mult(X,Y,U), mult(X,Z,Xt), mult(X,V,W) -> plus(U,Xt,W) . % mult right-distributes over plus goal plus(Y,Z,V), mult(Y,X,U), mult(Z,X,Xt), mult(V,X,W) -> plus(U,Xt,W). % some facts mult(a, b, c). % a*b=c mult(-(a), -(b), d). % (-a)*(-b)=d c=d -> []. /* Proof: ====== 3 : true,true,true -> B+(C+D)=B+C+D [axiom] 5 : 0= -(B)+B [axiom] 6 : B=0+B [axiom] 7 : B=B+0 [axiom] 12 : 0=0*B [axiom] 13 : 0=B*0 [axiom] 14 + true,true,true,true -> B*(C+D)=B*C+B*D [axiom] 15 + true,true,true,true -> (B+C)*D=B*D+C*D [axiom] 16 : c=a*b [axiom] 17 : d= -(a)* -(b) [axiom] 18 : c=d -> [axiom] 19 : a*b= -(a)* -(b) -> [reduction of 18 by [16,17]] 29 + B*0=B* -(C)+B*C [chaining of 5 from 14] 30 + 0*B= -(C)*B+C*B [chaining of 5 from 15] 31 + 0=B* -(C)+B*C [reduction of 29 by [13]] 32 + 0= -(B)*C+B*C [reduction of 30 by [12]] 63 + 0+B=C* -(D)+(C*D+B) [chaining of 31 from 3] 68 + B=C* -(D)+(C*D+B) [reduction of 63 by [6]] 115 + -(B)* -(C)+0=B*C [chaining of 32 from 68] 125 + -(B)* -(C)=B*C [reduction of 115 by [7]] 127 + false [reduction of 19 by [125,0]] Length = 21, Depth = 8 Total time: 2530 milliseconds Number of search inferences: 77 Number of kept clauses: 51 */