From a Computer Algebra Library to a System with an Equational Prover - Artificial Intelligence and Symbolic Computation - page 283

shows (ukbbGoalRem res) . ("\n\n"++) .
showsUKBBHistory (ukbbHistory res) "" :: String

where
res = proveByUKBBRefutation Infinity skolemArgs groupTask formula
formula = parse (" (exist [X] (P X)) &
(forall [X,Y] (P X & P Y ==> P (X*(i Y))))
==> P e & (forall [X] (P X ==> P (i X))) ")

Here Infinity means the infinite resource given to the goal, and skolemArgs
specify the way to add the operators appearing after skolemization. Our predi-
cate calculus formula is presented as a term built with the operators "exist" ,
..., "==>" , "P" , "*" , "i" . The proof starts by reducing the formula term. The
function proveByUKBBRefutation forms the negation, skolemizes it (extending
the theory to groupTask' ), converts it to a list of what we call btDisjuncts ,
each disjunct represented as a certain Boolean term ( BT )[2].A Theory also
keeps a list of BT. The formulas join the btLaws part of the theory in the form
of such a list. BT-s form an associative and commutative algebra, with the idem-
potence law, with respect to the operations xor , & . For more eciency, the prover
applies to BT a special completion method (the function ukbb ). Our example
yields the four disjuncts in a BT form:

btDisjuncts = [(P XSk) xor 1, (P (X*(i Y)))&(P Y)&(P X) xor (P Y)&(P X),
(P XSk0)&(P e) xor (P e), (P i XSk0)&(P e) ]

XSk, XSk0 are the constants returned by skolemization. btDisjuncts join
the theory, making it groupTask3 , and then there applies the completion:
ukbb _ groupTask3 ([],[1]) - “complete the equations and BT of the given
theory aiming at the BT goal [1] ”. Deriving a BT which reduces 1 to 0 would
mean a successful proof by refutation. ukbb combines the usual unfailing comple-
tion [3], [6] with the superpositions of kind equation+BT, BT+BT [2], and with
a special reduction on BT. It also accumulates a proof history . In our example,
the result prints as

ukbbGoalRem = ([],[]) -- [true] -> [false] -> [] done

History =
[[2] (P XSk) xor 1 [4] (P XSk0)&(P e) xor (P e)

[5] (P i XSk0)&(P e) [3] (P Y)&(P X)&(P (X*(i Y))) xor (P Y)&(P X)

[1] e*X -> X
[6] (P Y)&(P i Y)&(P e) xor (P Y)&(P e) from [1], [3] ...

[7] P ((i (Y0* i XSk))*Y0) from [..], [2] ...

[8] 1 from [1], [7] ]

The labels of type [Integer] serve as the references on print-out.
The ukbb method implements mainly the idea of RN+ strategy given in [2].
But Dumatel applies a stronger method for the BT reduction. This is based
on the monomial ordering by the monomial scheme : power product made of
the corresponding top predicate symbols. Its relation to graded algebras and
Grobner bases is a new computer algebra subject in our design.