# UKB Search for proofs of equational theorems, or compute a set of convergent rules using the [Unfailing Knuth-Bendix completion procedure](https://en.wikipedia.org/wiki/Knuth%E2%80%93Bendix_completion_algorithm). ## Quick Run The proof search can be run from the command line. Run ```bash $ node run ``` 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. Axioms and goals can also be extracted from a TPTP problem file such as GRP136-1.p, for instance. Note that package [tptp](https://www.npmjs.com/package/tptp) facilitates downloading such TPTP problems. Only pure equational problems in CNF can be processed. Supply options for such files in JSON format. See ```samples/options.json``` as an example. ## Usage ```js const ukb = require('ukb'); ``` ```ukb``` exposes the functions __createProver__ and __createTptpProver__: ### createProver (axioms, options) 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 optional parameter ```options``` should, if supplied, be an object with one or more of the following properties: * ```preorder```: see options of prover method ```run``` described below; the value of this option will be used unless overwritten when starting or restarting a prover run. * ```logger```: see options of prover method ```run``` described below; the value of this option will be used unless overwritten when starting or resuming a prover run. * ```logLevel```: see options of prover method ```run``` described below; the value of this option will be used unless overwritten when starting or resuming a prover run. * ```goals```: see options of prover method ```run``` described below; the goals provided here will always be included in the set of goals to be proved. 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 by ```getStatus``` (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 parameter ```options``` is optional. If it is supplied it must be an object with properties described below. Note that properties ```ordering```, ```preorder```, ```weighting```, ```indexingMatch```, and ```proofsEnabled``` 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. As a matter of fact this option is currently ignored. - ```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 property ```name```. Currently there is only one weighting function, namely weighted symbol count. Hence the value of property ```name``` can only be ```"weightedSymbolCount"``` or ```"WSC"``` for short. Use additional properties ```fctWeights``` and ```varWeight``` 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 of ```fctWeights``` can either be a number or an object. If it is a number, then that weight applies to all (non-variable) 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 is ```false```. Setting the value to ```true``` 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 option ```logLevel```. - ```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. Note that goals are added to the list of goals every time ```run``` is called. That is, previously given goals are not discarded. If you want a clean start, use ```rerun``` (see below). A goal can be negated, properly Skolemized, and presented as an inequality. For instance, commutativity ```f(x,y) = f(y,x)``` (for all ```x``` and ```y```) of a function symbol ```f``` is given as ```f(c1,c2) != f(c2,c1)```, where ```c1``` and ```c2``` are constants not occurring anywhere else. Alternatively the goal can be presented in a quantified, positive form, using ```!``` and ```?``` for universal and existential quantification, respectively. For instance, in group theory, the existence of a left-inverse element is given as ```!x?y: f(y,x) = a```, where ```a``` represents the neutral element. Commutativity is specified by ```!x,y: f(x,y) = f(y,x)```. In both cases the goals are properly Skolemized automatically. - ```tptpMode```: a Boolean value that, if _true_, indicates that TPTP-style (or Prolog-style) variable names will be used; otherwise, which is the default, variable names follow the conventions outlined above. - ```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 calling ```run(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 is ```false```. Note that a value of ```true``` 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. - ```cmpEqSidesForCpGen```: A Boolean value that indicates whether or not the two sides of an equation are to be compared before being used to create a critical pair. The default is ```false```. When set to ```true``` an (instance of an equation) will not be used if, as a result, a term would be replaced with a greater term (as per ordering). That way the generation of obsolete critical pairs is prevented. However, this leads to more comparison operations. - ```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 calling ```run(options)``` again with the same or different options. - ```proofsEnabled```: A Boolean value that, if _true_, switches on proof recording. As a result, goals that can be proved offer the possibility to obtain a proof in standard mathematical (human-readable) form. See ```getGoals()``` below for details. It should be noted that proof recording increases memory consumption and computation time, so it should not be switched on needlessly. * ```rerun(options)```: Discards all goals as well as all results from previous runs and restarts the prover; it is identical to calling ```run``` 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 through ```run``` or ```rerun``` the value returned is ```undefined```. 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 calling ```run(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 status ```completed``` 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```) - ```proof```: The proof (if found) as an object that has two functions ```toStringDetailed()``` and ```toString()``` that present the proof in a detailed and simple form, respectively, as a string in both cases - ```dsGoal```: The de-Skolemized goal as a string, generated by undoing Skolemization, which may not always be possible; if it is not possible then this property is ```null``` - ```dsProof```: The proof (if found) of the de-Skolmized goal (if it was generated) as an object that has two functions ```toStringDetailed()``` and ```toString()``` that present the proof in a detailed and simple form, respectively, as a string in both cases * ```getPreorder()```: Returns the current preorder as an array of symbols in descending order * ```getStatistics()```: Returns statistics for the current run (note that statistics are not reset when resuming a run using ```run(options)```); the value returned is an object with the following properties (all of which are non-negative 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 - ```obsoleteCritGoals```: The number of goals that were created, but not activated since one or both of the parents were not active goals anymore * ```getHrtimeElapsed()```: Returns the time elapsed since starting the most recent run in ```process.hrtime``` format * ```getTimeElapsed()```: Returns the time elapsed since starting the most recent run as a human-readable string * ```normalize(t)```: Returns the term obtained by normalizing ```t``` (i.e. computing the normal form of ```t``` w.r.t. the completed set of axioms). Both ```t``` and the term returned are strings. Note that an exception is thrown if the prover is not in status ```completed```. * ```testEquality(eq)```: Tests the given equality ```eq```, i.e. an equation ```s = t``` (a string). The result is ```true``` if the normal forms of ```s``` and ```t``` are identical, ```false``` otherwise. Note that an exception is thrown if the prover is not in status ```completed```. 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: ```js > const ukb = require('ukb'); undefined > let prover = ukb.createProver(['f(x,0)=x', 'f(x,i(x))=0', 'f(f(x,y),z)=f(x,f(y,z))'], {preorder:['i','f','0']}); undefined ``` This prover can then be run to obtain a convergent set of rules: ```js > prover.run(); 'completed' > prover.getStatus(); 'completed' > prover.getRules(); [ '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.getEquations(); [] ``` You may re-use 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)```: ```js > prover.run({goals:['f(x,g(x)) != g(x)']}); 'completed' > prover.getGoals(); [{ goal: 'f(x,g(x)) != g(x)', proved: true, proof: null, dsGoal: '?v1!v2: f(v1,v2) = v2', dsProof: null }] ``` 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). Note also that there are no proofs because proof recording was not switched on. There is, however, a de-Skolemized version of the original goal. 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. We switch on proof recording for this run so that we can have a look at the proof found: ```js > prover.rerun({goals:['f(x,g(x)) != g(x)'], proofsEnabled:true}); 'proved' > prover.getStatus(); 'proved' > prover.getRules(); [ '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.getGoals(); [{ goal: 'f(x,g(x)) != g(x)', proved: true, proof: { ... }, dsGoal: '?v1!v2: f(v1,v2) = v2', dsProof: { ... } }] ``` 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 so-called critical goal ```g(0) != g(0)``` which proves the goal by contradiction. Since proof recording was switched on we can now have a look at the detailed proof of the de-Skolemized goal, for instance: ```js > console.log(prover.getGoals()[0].dsProof.toStringDetailed()); f(0,v2) = f(0,f(v2,0)) : x = f(x,0) at position 2 with x <- v2 = f(0,f(v2,f(i(v2),i(i(v2))))) : 0 = f(x,i(x)) at position 2.2 with x <- i(v2) = f(0,f(f(v2,i(v2)),i(i(v2)))) : f(x,f(y,z)) = f(f(x,y),z) at position 2 with x <- v2, y <- i(v2), z <- i(i(v2)) = f(0,f(0,i(i(v2)))) : f(x,i(x)) = 0 at position 2.1 with x <- v2 = f(f(0,0),i(i(v2))) : f(x,f(y,z)) = f(f(x,y),z) at position root with x <- 0, y <- 0, z <- i(i(v2)) = f(0,i(i(v2))) : f(x,0) = x at position 1 with x <- 0 = f(f(v2,i(v2)),i(i(v2))) : 0 = f(x,i(x)) at position 1 with x <- v2 = f(v2,f(i(v2),i(i(v2)))) : f(f(x,y),z) = f(x,f(y,z)) at position root with x <- v2, y <- i(v2), z <- i(i(v2)) = f(v2,0) : f(x,i(x)) = 0 at position 2 with x <- i(v2) = v2 : f(x,0) = x at position root with x <- v2 undefined ``` The explanation or justification following the colon details the step taken to transform the term of the previous line into the term before the colon. Note that all justifications use only (instances of) axioms. 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'```: ```js > prover.run({goals:['f(a,b)!=f(b,a)']}); 'completed' > prover.getGoals(); [{ goal: 'f(x,g(x)) != g(x)', proved: true, proof: { ... }, dsGoal: '?v1!v2: f(v1,v2) = v2', dsProof: { ... } }, { goal: 'f(a,b) != f(b,a)', proved: false, proof: null, dsGoal: '!v1,v2: f(v2,v1) = f(v1,v2)', dsProof: null }] > prover.getStatus(); 'completed' ``` This example also demonstrates that calling ```run``` does not discard previously given goals, and that proof recording remains active because it was switched on through ```rerun``` and cannot be changed when resuming the procedure through ```run```. The same result without proof recording can be achieved as follows: ```js > prover.rerun({goals:['f(x,g(x)) != g(x)', 'f(a,b)!=f(b,a)']}); 'completed' > prover.getGoals(); [{ goal: 'f(x,g(x)) != g(x)', proved: true, proof: null, dsGoal: '?v1!v2: f(v1,v2) = v2', dsProof: null }, { goal: 'f(a,b) != f(b,a)', proved: false, proof: null, dsGoal: '!v1,v2: f(v2,v1) = f(v1,v2)', dsProof: null }] > prover.getStatus(); 'completed' ``` ### createTptpProver (tptpProblem, options) The function returns an object representing a prover that extracts axioms and possibly goals from a TPTP problem. Parameter ```tptpProblem``` must be the contents of a TPTP problem (i.e., a string) with all include statements resolved. Note that package [tptp](https://www.npmjs.com/package/tptp) facilitates downloading such TPTP problems. Only pure equational problems in CNF can be processed. Axioms and goal(s) are extracted from the TPTP problem. For a description of parameter ```options``` as well as the functions of the prover object returned consult the documentation of __createProver__.