# CONDET

Search for proofs of propositional theorems using
[Condensed Detachment](http://en.wikipedia.org/wiki/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](http://www.tptp.org/), 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
```bash
$ 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.
```bash
P e(?,+):20
```
or
```bash
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
```bash
$ node rnd
```
for usage information.

## Usage
```js
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](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.379.8524&rep=rep1&type=pdf)), 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](http://en.wikipedia.org/wiki/Condensed_detachment#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](https://www.npmjs.com/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](http://en.wikipedia.org/wiki/Condensed_detachment#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](https://www.npmjs.com/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](http://www.tptp.org/cgi-bin/SystemOnTPTP)
or as parameter ```problem``` to functions ```runSystem```, ```runSuggestedSystem```,
and ```runParallel``` of package [tptp](https://www.npmjs.com/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```).

