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. LCL007-1.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 so-called 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 Two-Valued 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 by getState() (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 property logLevel); in the simplest case use logger: 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 a logger, 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 or depthWeight = 3 while leaving symbolWeight = 1) may steer the search towards shorter proofs that are found faster. (See, for instance, samples r02.cds, ec03.cds, or mv03.cds.)

  • symbolWeight: the weight for the symbol component of the heuristic weight; default: 1

  • indexing: a flag that if true 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 if true 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 if true 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 as e(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 if true 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 (see separate() and searchToString() in the context of getProofs() 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 attributes pattern and mod, and a list of patterns is an array of such objects. The value of attribute pattern 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 attribute mod 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 created prover it behaves exactly as rerun. Otherwise it resumes where a previous run left off and only accepts option properties timeout and maxActivations. 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 functions run and rerun); 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. option maxActivations)

  • 'timeout': a specfied timeout was exceeded (cp. option timeout)

• 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 parameter axioms of createProver) as an array of strings

• getGoals(): returns the goals for the prover (as per parameter goals of createProver) 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 returns true 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 in process.hrtime format

• getTimeElapsed(): returns the time elapsed during the most recent run as a human-readable string

• getProcessTotalTime(): returns the total (aggregated) time elapsed during all runs (since the most recent restart) in process.hrtime format

• getTotalTime(): returns the total (aggregated) time elapsed during all runs as a human-readable 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 by getSteps()

  • 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 by getLength()

  • getProcessTimeElapsed(): returns the time elapsed to find this proof in process.hrtime format

  • getTimeElapsed(): returns the time elapsed to find this proof as a human-readable string

  • toDNotation(asObj): returns the proof in D-notation; if parameter asObj is false (or not supplied) the value returned is a string showing axioms and D-notation of fact proved (and the fact proved itself) in a convenient form; otherwise the value returned is an object with properties axioms (an array of strings representing the axioms used), dNotation (a string representing the proof in D-notation, its indices tied to the positions of axioms in the array), provenFact (the fact proved as a string), and a convenience function toString() that converts the object into a string representation (which is the same as the string returned when parameter asObj is false)

  • toString(): returns the proof in a human-readable 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 option recordSearch is true (see description of options of prover methods run and rerun)

  • separate(): returns an object with two properties pos and neg 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 option recordSearch is true (see description of options of prover methods run and rerun)

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 D-notation). 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 property logLevel); in the simplest case use logger: 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 a logger, 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 D-notation); default: 1

• maxDepth: the maximal depth of a random proof (in D-notation); default: 10

• probabilityD: the probability to create a D-node (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 depth maxDepth, whereas smaller values tend to produce random proofs with a depth closer to the minimal depth minDepth; 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 in process.hrtime format

• timeElapsed: the time elapsed as a human-readable 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 property state 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 by getSteps()

  • 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 by getLength()

  • toDNotation(asObj): the proof in D-notation; if parameter asObj is false (or not supplied) the value returned is a string showing axioms and D-notation of fact proved (and the fact proved itself) in a convenient form; otherwise the value returned is an object with properties axioms (an array of strings representing the axioms used), dNotation (a string representing the proof in D-notation, its indices tied to the positions of axioms in the array), provenFact (the fact proved as a string), and a convenience function toString() that converts the object into a string representation (which is the same as the string returned when parameter asObj is false)

  • toString(): the proof in a human-readable 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).