UKB
Search for proofs of equational theorems, or compute a set of convergent rules using the Unfailing KnuthBendix completion procedure.
Installation
$ npm install ukb
Quick Run
The proof search can be run from the command line. Run
$ node tests/runukb
for usage information.
Axioms and goals (i.e., theorems to be proved) are specified in a file.
Samples of such files can be found in directory samples
. Consult
in particular samples/group_prove.eqs
for details on the notation
used in such a file.
Usage
var ukb = ;
ukb
exposes the following function:
createProver (axioms)
The function returns an object representing a prover. It has one mandatory parameter axioms
, the axioms given as an array of strings, or a string in case of a single axiom. Each axiom (string) is an equation, e.g. f(i(x),x) = a
. Note that a symbol starting with the letter
x, y, z, u, v, or w, optionally followed by one or more digits, is assumed to be a variable. Variables are
implicitly universally quantified. All other symbol names denote functions or constants.
For standard group axiomatization use, for instance,
['f(x,a) = x', 'f(x,i(x)) = a', 'f(f(x,y),z) = f(x,f(y,z))']
as a possible value of parameter axioms
.
The prover object returned has the following functions:

run(options)
: Starts or resumes a proof search or an attempt to produce a convergent set of rules (completion); the return value is the status at the time the run is terminated. It is the same value that is also returned bygetStatus
(see below). A run can be terminated before all proofs are found or completion succeeded using options described below. A run can be resumed by calling this function any number of times. The parameteroptions
is optional. If it is supplied it must be an object with properties described below. Note that propertiesordering
,preorder
,weighting
, andindexingMatch
are taken into account only if a run starts from scratch (i.e., does not resume from where a previous run left off).
ordering
: The ordering to be used. Currently there is only one ordering (Lexicographic Path Ordering or LPO) which makes using this option obsolete. 
preorder
: Defines the preorder employed by the chosen ordering (which can only be the LPO at this stage). The preorder is given as an array of symbol names where one symbol is greater than another if its array index is smaller (i.e., it occurs before the other in the array). The preorder may be partial or may be omitted altogether. If a symbol is encountered that is not in the preorder it is appended to the preorder as the (at that moment) smallest symbol. 
weighting
: A specification of the heuristic weighting function for selecting the next critical pair to become a rule or an equation; if omitted standard weighted symbol count is employed where variables count as 1 and all other symbols as 2. Otherwise the weighting function is specified through an object that must have propertyname
. Currently there is only one weighting function, namely weighted symbol count. Hence the value of propertyname
can only be"weightedSymbolCount"
or"WSC"
for short. Use additional propertiesfctWeights
andvarWeight
to specify the weights of functions and variables, respectively. (If omitted, the default weights will be used, which are 2 for function symbols and 1 for variables as mentioned above.) The value offctWeights
can either be a number or an object. If it is a number, then that weight applies to all (nonvariable) symbols. If it is an object then symbol names are properties and weights (i.e., numbers) their values. 
indexingMatch
: A Boolean value that indicates whether an indexing technique should be employed for matching attempts (i.e., reductions); the default isfalse
. Setting the value totrue
in most cases leads to significant performance improvements. Deterioration can only be expected for problems requiring very little time to solve (i.e., when the overhead outweighs the gains). Note, however, that switching on indexing may change the search behavior on account of a different order in which rules or equations are used for reductions. 
logger
: A function accepting one (string) parameter (e.g.,console.log
); the function will be called with information that can be logged. The level of detail of that information depends on optionlogLevel
. 
logLevel
: An integer ranging from 0 to 6 that denotes the detail level of logging; higher values produce more logging information. The default is 0 which produces no logging information at all. 
goals
: The goals to be proved, given as a string (if there is but one goal) or an array of strings; each goal must be negated, properly Skolemized, and presented as an inequality. For instance, commutativityf(x,y) = f(y,x)
(for allx
andy
) of a function symbolf
, if it were to follow from the axioms, is given asf(c1,c2) != f(c2,c1)
, wherec1
andc2
are constants not occurring anywhere else. Note that goals are added to the list of goals to be proved every timerun
is called. That is, previously given goals are not discarded. If you want a clean start, usererun
(see below). 
maxActivations
: The maximal number of activations after which the run terminates; each rule or equation generated as well as each goal activated counts as one activation. If omitted or not greater than 0 there will be no limit on the number of activations. Note that a run terminated this way can be resumed by callingrun(options)
again with the same or different options. 
reduceCpBeforeAdding
: A Boolean value that indicates whether or not a critical pair is reduced before adding it to the set of critical pairs; the default isfalse
. Note that a value oftrue
typically increases the total number of reductions, but reduces the number of critical pairs added. However, by reducing critical pairs beforehand their weight may change which may affect the search behavior one way or the other. 
timeout
: A timeout (in milliseconds) after which the run terminates; if omitted or not greater than 0 there will be no timeout. Note that a run terminated this way can be resumed by callingrun(options)
again with the same or different options.


rerun(options)
: Discards all goals as well as all results from previous runs and restarts the prover; it is identical to callingrun
on a prover that was just created (i.e., has not yet run). 
getStatus()
: Returns the status of the proof procedure; if the prover has never been started throughrun
orrerun
the value returned isundefined
. Otherwise it can have one of the following string values:
stopped
: A timeout occurred or the maximal number of activations was reached; resume the search by callingrun(options)
with the appropriate options. 
proved
: All goals were proved (but no convergent set of rules was computed) 
completed
: A convergent set of rules was computed; note that statuscompleted
implies that all goals were either proved or disproved.


getRules()
: Returns the current set of rules as an array of strings 
getEquations()
: Returns the current set of equations as an array of strings 
getGoals()
: Returns the current set of goals as an array of objects, where each such object has the following properties:
goal
: The goal as a string 
proved
: Boolean flag indicating whether the goal was proved (true
) or not (false
)


getStatistics()
: Returns statistics for the current run (note that statistics are not reset when resuming a run usingrun(options)
); the value returned is an object with the following properties (all of which are nonnegative integers):
rulesAdded
: The number of rules added 
equationsAdded
: The number of equations added 
rulesDiscarded
: The number of rules removed from the set of rules and added to the set of critical pairs (on account of reducing the left side) 
equationsDiscarded
: The number of equations removed from the set of equations and added to the set of critical pairs (on account of reducing either side) 
reductions
: The total number of reductions 
cmpCount
: The total number of term comparisons (using the chosen term order) 
cpAdded
: The number of critical pairs added to the set of critical pairs 
cpGenerated
: The number of critical pairs generated through overlapping; note that axioms also become critical pairs, but are not generated. 
obsoleteCp
: The number of critical pairs selected for processing, but discarded since one or both parents were not active rules or equations anymore 
trivialCp
: The number of critical pairs selected for processing, but discarded since they could be reduced to a trivial equation (i.e., identity) 
fwdSubsumption
: The number of equations rejected since they were subsumed by an existing equation 
bwdSubsumption
: The number of equations discarded since they were subsumed by a newer equation 
goalsActivated
: The number of goals activated (i.e., taking an active part in reductions and generation of further critical goals) 
critGoalsCreated
: The number of critical goals created (by overlapping rules or equations into activated goals) 
goalsFwdSubsumed
: The number of goals about to be activated, but rejected since they were subsumed by previously activated goals 
goalsBwdSubsumed
: The number of activated goals that were removed since they were subsumed by a new (active) goal


getHrtimeElapsed()
: Returns the time elapsed since starting the most recent run inprocess.hrtime
format 
getTimeElapsed()
: Returns the time elapsed since starting the most recent run as a humanreadable string 
normalize(t)
: Returns the term obtained by normalizingt
(i.e. computing the normal form oft
w.r.t. the completed set of axioms). Botht
and the term returned are strings. Note that an exception is thrown if the prover is not in statuscompleted
. 
testEquality(eq)
: Tests the given equalityeq
, i.e. an equations = t
(a string). The result istrue
if the normal forms ofs
andt
are identical,false
otherwise. Note that an exception is thrown if the prover is not in statuscompleted
. Note also that this simple test can only handle universally quantified variables. These variables have to be replaced with Skolem constants if there are equations after completing the set of axioms. Do not use this simple test in the presence of existentially quantified variables. Instead, run the prover and add the respective goal as described above. (See also the following examples.)
Examples
We assume that module or package ukb has been installed. A prover object for standard group axiomatization is created this way:
> var ukb = ;undefined> var prover = ukb;undefined
This prover can then be run to obtain a convergent set of rules:
> prover;'completed'> prover;'completed'> prover; 'f(x,0) > x' 'f(x,i(x)) > 0' 'f(f(x,y),z) > f(x,f(y,z))' 'f(y,f(i(y),x)) > x' 'f(0,x) > x' 'i(0) > 0' 'f(i(x),x) > 0' 'i(i(x)) > x' 'f(i(x),f(x,y)) > y' 'i(f(y,x)) > f(i(x),i(y))' > prover;
You may reuse the convergent set of rules to prove one or more goals. In this example
we prove that there is an x
so that for all y
it is true that f(x,y) = y
.
After negation and Skolemization this goal is converted into the inequality
f(x,g(x)) != g(x)
:
> prover;'completed'> prover; goal: 'f(x,g(x)) != g(x)' proved: true
Note that the return value of the second run also is 'completed'
(which entails,
as explained above, that any goal can be either proved or disproved). If, on the other hand,
you rerun the prover with that goal, the return value is 'proved'
as the proof procedure
stops as soon as all goals (in this case just one) are proved (which happens before a convergent
set of rules was obtained):
> prover;'proved'> prover;'proved'> prover; 'f(x,0) > x' 'f(x,i(x)) > 0' 'f(f(x,y),z) > f(x,f(y,z))' 'f(x,i(0)) > x' 'f(x,f(y,i(f(x,y)))) > 0' 'f(y,f(i(y),x)) > x' 'f(x,f(i(0),y)) > f(x,y)' 'f(x,i(i(y))) > f(x,y)' 'f(0,x) > x' > prover; goal: 'f(x,g(x)) != g(x)' proved: true
The set of rules available at the time of proving the goal is not yet a convergent set of rules.
The set does, however, contain the rule that is essential for proving the goal, namely
the last (i.e., the most recently created) rule f(0,x) > x
, which through overlapping
with the goal (unification of f(0,x)
and f(x,g(x))
)
produces the goal instance f(0,g(0)) != g(0)
. That goal instance leads to the socalled critical
goal g(0) != g(0)
which proves the goal by contradiction.
When adding a goal that cannot be proved, e.g. commutativity of f
, then a (re)run
will only stop as soon as a convergent set of rules has been obtained, and therefore the return
value as well as the status of the proof run is 'completed'
:
> prover;'completed'> prover; goal: 'f(x,g(x)) != g(x)' proved: true goal: 'f(a,b) != f(b,a)' proved: false > prover;'completed'
This example also demonstrates that calling run
does not discard previously
given goals. The same result can be achieved as follows:
> prover;'completed'> prover; goal: 'f(x,g(x)) != g(x)' proved: true goal: 'f(a,b) != f(b,a)' proved: false > prover;'completed'