CONDET
Search for proofs of propositional theorems using Condensed Detachment.
Quick Run
The scripts prove.js
and rnd.js
described below provide a convenient access to the available search
procedures from the command line. All scripts can read their input from sample files.
Sample files use a simple syntax to provide axioms, goals, a specification of the inference rule
(if necessary), and possibly settings for search parameters.
Sample files can be found in directory samples
. You may of course write your own sample files.
Note that a line starting with A
defines an axiom, a line starting with G
a goal (theorem),
and a line starting with R
specifies the inference rule to be used by its name (i.e., use
either R Std
or R AN
, which is only necessary if the appropriate inference rule cannot be determined
automatically; cp. parameter infRule
of functions createProver
and createRndProver
described below).
Lines starting with a character that is not recognized are simply ignored.
The scripts can also be applied to problems of the TPTP, specifically to problems of domain LCL. If such a problem name is given, e.g. LCL0071.p (assuming you have a local copy of that file), axioms, goals, and inference rule are extracted from the problem description.
Forward Reasoning
prove.js
can be used to execute the search procedure based on forward reasoning
on a given list of sample files (files containing axioms and goals, a.k.a. theorems)
or TPTP problems (see createProver and createTptpProver below). Run
$ node prove
for usage information.
Apart from lines starting with A
, G
, or R
specifying axioms, goals, or inference
rule, respectively (cp. description of sample files above), sample files for prove.js
may also specify certain parameters of the search procedure (also referred to as options).
A line starting with W
should be followed by two numbers separated
by a colon to specify the symbol and depth weight (in that order).
Note that any weights given this way are overridden by the w
option (cf. description of options
symbolWeight
and depthWeight
below).
Every line starting with P
defines a socalled pattern, e.g.
P e(?,+):20
or
P e(?,+):w => w * 2
(cf. description of option patterns
below).
Random Search
rnd.js
can be used to execute a random search for a proof (see createRndProver and
createRndTptpProver below). Run
$ node rnd
for usage information.
Usage
const cd = require('condet');
Prove theorems using
cd.createProver
cd.createTptpProver
cd.createRndProver
cd.createRndTptpProver
Use cd.tptpFormat
to convert axioms, goals, and rule of inference into a TPTP problem.
createProver (axioms, goals, infRule)
Creates an object prover
for searching for proofs of the given goals (theorems)
using the given axioms. Axioms and goals can
be specified through a string separating axioms or goals with a newline character \n
,
or through an array of strings.
The search procedure is based on enumerating facts derived from the axioms (Forward Reasoning). The enumeration of facts is guided by a heuristic based on a weighted sum of symbol count and derivation depth. A goal is proved if a fact is derived that is identical to, or more general than, the goal.
The rule of inference can be supplied through parameter infRule
. Use the strings 'Std'
or 'AN'
for standard condensed detachment (modus ponens) or
a slightly modified rule that takes into account the syntactic pecularities of the
AN Calculus (Disjunction/Negation TwoValued Sentential Calculus), respectively. For any other value (or no value) the rule
of inference is determined automatically. That means, a value only needs to be supplied if the automatic
determination of the rule of inference does not yield the expected result (see prover.getInfRuleId
and
prover.getInfRuleName
described below).
The following functions can be called on prover
to start, continue, or restart the proof search, as well
as to obtain information on the current state of the proof search:

rerun(options)
: starts or restarts a proof run from scratch, discarding previous runs (if any). The return value is the state at the time the run terminates. It is the same value as is returned bygetState()
(see below). Options may be supplied as an object where the following properties are recognized:
logger
: a function that accepts a string as a parameter and logs it in an appropriate way (the amount of data logged is determined by propertylogLevel
); in the simplest case uselogger: console.log
; default: no logging 
logLevel
: the log level (a number ranging from 0 to 6) that determines the degree of detail of logging activities (logging takes place only in the presence of alogger
, of course); as usual a bigger number means more data logged; default: 0 (nothing will be logged) 
depthWeight
: the weight for the depth component of the heuristic weight; default: 0. Note that a moderate integration of depth (e.g.,depthWeight = 2
ordepthWeight = 3
while leavingsymbolWeight = 1
) may steer the search towards shorter proofs that are found faster. (See, for instance, samplesr02.cds
,ec03.cds
, ormv03.cds
.) 
symbolWeight
: the weight for the symbol component of the heuristic weight; default: 1 
indexing
: a flag that iftrue
enables term indexing for the purpose of speeding up forward subsumption, or in other words for significantly increasing the efficiency of finding an active fact that subsumes a freshly created fact; default:false

precheckGoalSubsumption
: a flag that iftrue
indicates that every fact created through condensed detachment should be checked for matching (and hence proving) a goal; default:false
. Note that setting this flag incurs a performance penalty due to the additional matching effort, but can shorten the search if (and only if) activation of the very last fact that proves a goal is delayed due to redundant facts that are preferred on account of their heuristic weight (or FIFO position). 
checkUselessAsMajorPremise
: a flag that iftrue
indicates that every active fact is checked to ascertain whether it is sensible to use it as a major premise; default:false
. The idea is to mark a fact such ase(x,x)
as unsuitable as a major premise because it simply copies the minor premise. Note, however, that the gains in terms of reduced redundancy are more often than not outweighed by the additional checking effort. 
recordSearch
: a flag that iftrue
causes the search procedure to record all activated facts; as a result all proofs found offer the possibility to examine positive and negative facts (i.e., facts used and not used in the proof, respectively), and to view the full search (seeseparate()
andsearchToString()
in the context ofgetProofs()
below) 
patterns
: a pattern or a list of patterns that are used to modify the heuristic weight of facts and hence the search; a pattern is an object with attributespattern
andmod
, and a list of patterns is an array of such objects. The value of attributepattern
is a string that defines a term, or rather a set of terms, using function symbols and special symbols'?'
,'+'
, and'*'
as leaf nodes.'?'
stands for any variable,'+'
for any term except a variable, and'*'
for any term. The value of attributemod
is either a number or a function that takes a number as an argument and returns a number. The purpose of such a function is to modify a given heuristic weight and return the modified value. Providing a number as a value is a way of adding that number to the original heuristic weight without the need to define a function. A heuristic weight of a fact is modified if the respective pattern matches that fact. The first pattern to match is employed. Possible further matching patterns are ignored. For instance, the following pattern adds 20 to the original heuristic weight of any fact e(T1,T2) where T1 is a variable and T2 is not a variable:{pattern:'e(?,+)', mod:20}
which is equivalent to{pattern:'e(?,+)', mod:w => w + 20}
. If instead of adding 20 you prefer to multiply the original heuristic weight by 2 then use:{pattern:'e(?,+)', mod:w => w * 2}
. Naturally, the application of patterns incurs a performance penalty. However, the reduced search effort may outweigh that performance penalty. 
timeout
: timeout in milliseconds; values of 0 or less are ignored; default: 1 (no timeout) 
maxActivations
: the maximal number of facts to be activated; values less than 0 mean no limit; default: 1 (no limit)


run(options)
: if called on a freshly createdprover
it behaves exactly asrerun
. Otherwise it resumes where a previous run left off and only accepts option propertiestimeout
andmaxActivations
. If not supplied the default behavior is employed, i.e. no timeout and no limit on the number of active facts is imposed, respectively. 
getState()
: returns the state of the search after the most recent run (also returned by functionsrun
andrerun
); its value is one of the following strings:
'failure'
: one or more goals cannot be proved; this state is an indication that there is an issue with the axiomatization and/or an unsuitable inference rule was chosen 
'success'
: all goals could be proved 
'stopped'
: the search was stopped because the specified maximal number of active facts was exceeded (cp. optionmaxActivations
) 
'timeout'
: a specfied timeout was exceeded (cp. optiontimeout
)


getStatistics()
: returns statistical information through an object with the following properties (note that a passive fact represents a fact that is known to follow from the current set of active facts, but has not yet been activated (i.e. it has not yet participated in the derivation of new facts):
parentSubsumptions
: the number of (passive) facts discarded because one or both parents (i.e, major and minor premise) had been removed on account of backward subsumption 
forwardSubsumptions
: the number of forward subsumptions 
backwardSubsumptions
: the number of backward subsumptions 
linksCreated
: the total number of facts (passive and active) created 
activated
: the number of activated facts 
condetFailures
: the number of attempted applications of the inference rule to a major and minor premise that failed (i.e., unification was not possible) 
fwdMatchingFailures
: the number of failed matching attempts in the context of forward subsumption 
bwdMatchingFailures
: the number of failed matching attempts in the context of backward subsumption 
goalMatchingFailures
: the number of failed matching attempts in the context of goal subsumption


getStatisticsAsString()
: returns statistical information as a formatted string 
getAxioms()
: returns the axioms available to the prover (as per parameteraxioms
ofcreateProver
) as an array of strings 
getGoals()
: returns the goals for the prover (as per parametergoals
ofcreateProver
) as an array of strings 
addGoal(goal)
: adds a new goal (given as a string) to the current set of goals; the goal is ignored if an identical goal exists in the set of goals. This function returnstrue
if the goal was added,false
otherwise. A goal will instantaneously be proved, and a proof will be available, if the goal is subsumed by one of the active facts. 
getInfRuleId()
: the identifier of the rule of inference used; the value will be either'Std'
or'AN'

getInfRuleName()
: the name of the rule of inference used; the value will be either'Standard'
or'AN Calculus'

getGoalsProved()
: returns the goals that were proved as an array of strings 
getGoalsProvedCount()
: returns the number of goals that were proved 
getGoalsNotProved()
: returns the goals that are not proved as an array of strings 
getGoalsNotProvedCount()
: returns the number of goals that are not proved 
getProcessTimeElapsed()
: returns the time elapsed during the most recent run inprocess.hrtime
format 
getTimeElapsed()
: returns the time elapsed during the most recent run as a humanreadable string 
getProcessTotalTime()
: returns the total (aggregated) time elapsed during all runs (since the most recent restart) inprocess.hrtime
format 
getTotalTime()
: returns the total (aggregated) time elapsed during all runs as a humanreadable string 
getProofs()
: returns the proofs found as an array of proof objects; each proof object offers the following functions:
getAxioms()
: returns the axioms used in this proof (as an array of strings) 
getGoal()
: returns the goal or theorem that was to be proved (as a string) 
getProvedBy()
: returns the fact that eventually proved the goal (as a string) 
getLength()
: returns the length of the proof (the number of axioms and inferred facts that constitute the proof); subtract the number of axioms involved in the proof and you obtain the steps of the proof as returned bygetSteps()

getDepth()
: returns the depth of the proof (the maximal distance from axioms in terms of inference steps, or in other words the depth of the proof viewed as a directed acyclic graph) 
getSteps()
: returns the number of inference steps (i.e., the number of applications of the inference rule) required for this proof; add the number of axioms involved in the proof and you obtain the length of the proof as returned bygetLength()

getProcessTimeElapsed()
: returns the time elapsed to find this proof inprocess.hrtime
format 
getTimeElapsed()
: returns the time elapsed to find this proof as a humanreadable string 
toDNotation(asObj)
: returns the proof in Dnotation; if parameterasObj
isfalse
(or not supplied) the value returned is a string showing axioms and Dnotation of fact proved (and the fact proved itself) in a convenient form; otherwise the value returned is an object with propertiesaxioms
(an array of strings representing the axioms used),dNotation
(a string representing the proof in Dnotation, its indices tied to the positions of axioms in the array),provenFact
(the fact proved as a string), and a convenience functiontoString()
that converts the object into a string representation (which is the same as the string returned when parameterasObj
isfalse
) 
toString()
: returns the proof in a humanreadable form (as a string) 
searchToString()
: returns a string that lists the full search detailing all activated facts and marking the positive facts (used for the proof eventually found) with+++
; this function is only available if optionrecordSearch
istrue
(see description of options of prover methodsrun
andrerun
) 
separate()
: returns an object with two propertiespos
andneg
which are arrays holding the positive and negative facts (as strings) for the respective proof, where positive facts are the facts used in the proof, and negative facts are all other (redundant) facts that played an active role during the search for a proof; this function is only available if optionrecordSearch
istrue
(see description of options of prover methodsrun
andrerun
)

createTptpProver (tptpProblem)
Creates an object prover
for searching for a proof of the given TPTP problem. More specifically tptpProblem
is the contents of a TPTP problem file (i.e., a string) without any include statements. Axioms, goals, and inference
rule will be extracted from that problem specification. If the conversion succeeds object prover
can be
used as if returned by createProver. Hence, see createProver for a description of prover
.
Note that package tptp facilitates downloading TPTP problems.
createRndProver (axioms, goal, infRule)
Creates an object prover
for searching for proofs of the given goal (theorem)
using the given axioms. Axioms can
be specified through a string separating axioms with a newline character \n
,
or through an array (of strings). The search procedure is based on random generation
of potential proofs (in Dnotation). The number of randomly generated proofs is limited
(cp. option maxIterations
).
The rule of inference can be supplied through the optional parameter infRule
analogous to the
equally named parameter of createProver
(see above). Use prover.getInfRuleId()
to obtain the identifier of the rule of inference used; the value will be either 'Std'
or 'AN'
. Use prover.getInfRuleName()
to obtain the name of the rule of inference used; the value will be either 'Standard'
or 'AN Calculus'
.
Retrieve the axioms as an array of strings and the goal as a string through prover.getAxioms()
and
prover.getGoal()
, respectively.
Start the random search any number of times
by calling prover.run(options)
. Options may be supplied as an object
where the following properties are recognized:

logger
: a function that accepts a string as a parameter and logs it in an appropriate way (the amount of data logged is determined by propertylogLevel
); in the simplest case uselogger: console.log
; default: no logging 
logLevel
: the log level (a number ranging from 0 to 4) that determines the degree of detail of logging activities (logging takes place only in the presence of alogger
, of course); as usual a bigger number means more data logged; default: 0 (nothing will be logged) 
maxIterations
: the maximal number of random proofs that will be generated; default: 100 
minDepth
: the minimal depth of a random proof (in Dnotation); default: 1 
maxDepth
: the maximal depth of a random proof (in Dnotation); default: 10 
probabilityD
: the probability to create a Dnode (i.e., an inner node, as opposed to a leaf, i.e. a reference to an axiom); higher values steer the random creation towards the maximal depthmaxDepth
, whereas smaller values tend to produce random proofs with a depth closer to the minimal depthminDepth
; default: 0.5
The return value of prover.run(options)
is an object that has the following properties:

iterations
: the number of randomly generated proofs 
processTimeElapsed
: the time elapsed inprocess.hrtime
format 
timeElapsed
: the time elapsed as a humanreadable string 
state
: the state of the search, which will be either'success'
or'failure'

proof
: this property is defined only if a proof was found (which is the case if and only if propertystate
holds the value'success'
); if it is defined it represents the proof found and offers the following functions:
getAxioms()
: the axioms used in this proof (as an array of strings) 
getGoal()
: the goal or theorem that was to be proved (as a string) 
getProvedBy()
: the fact that eventually proved the goal (as a string) 
getLength()
: the length of the proof (the number of axioms and inferred facts that constitute the proof); subtract the number of axioms involved in the proof and you obtain the steps of the proof as returned bygetSteps()

getDepth()
: the depth of the proof (the maximal distance from axioms in terms of inference steps, or in other words the depth of the proof viewed as a directed acyclic graph) 
getSteps()
: the number of inference steps (i.e., the number of applications of the inference rule) required for this proof; add the number of axioms involved in the proof and you obtain the length of the proof as returned bygetLength()

toDNotation(asObj)
: the proof in Dnotation; if parameterasObj
isfalse
(or not supplied) the value returned is a string showing axioms and Dnotation of fact proved (and the fact proved itself) in a convenient form; otherwise the value returned is an object with propertiesaxioms
(an array of strings representing the axioms used),dNotation
(a string representing the proof in Dnotation, its indices tied to the positions of axioms in the array),provenFact
(the fact proved as a string), and a convenience functiontoString()
that converts the object into a string representation (which is the same as the string returned when parameterasObj
isfalse
) 
toString()
: the proof in a humanreadable form (as a string)

createRndTptpProver (tptpProblem)
Creates an object prover
to perform a random search for a proof of the given TPTP problem.
More specifically tptpProblem
is the contents of a TPTP problem file (i.e., a string) without any include statements. Axioms, goals, and inference
rule will be extracted from that problem specification. If the conversion succeeds object prover
can be
used as if returned by createRndProver. Hence, see createRndProver for a description of prover
.
Note that package tptp facilitates downloading TPTP problems.
tptpFormat (axioms, goals, infRule)
Converts the given axioms and goals into TPTP format (cnf).
The result of the conversion is a string
(all clauses are separated by a newline character)
that can be given as input to
System on TPTP
or as parameter problem
to functions runSystem
, runSuggestedSystem
,
and runParallel
of package tptp.
Axioms and goals can be supplied as
an array of strings or a single string (if there is only one axiom or goal). The rule of
inference is optional. If not supplied it is determined automatically (cp. parameter
infRule
of createProver
).