# ProverX Scripting Library
The ProverX Scripting Library is a collection of modules and classes written in Python that are automatically imported in ProverX. They allow the user to interact easily with prover9 and mace4, launch simultaneous jobs, work with proofs, models, hints, etc.
# Table of Contents
[TOC]
----
# Class Proverx
This is the main class of ProverX. It opens files with prover9 syntax or the new advanced syntax (see Preprocessor Class) and tries to find proofs or models.
Example of usage:
```python
p = Proverx('abelian.in')
print p.axioms
print p.goals
print "Proofs found:"
print p.find_proofs()
print p.proofs
p.axioms.pop()
print p.find_proofs() #should print 0
p.find_models()
# This is the smallest non commutative group
# Just change max_models option to find more (ex. 20)
p.set_option('Mace4','assign','max_models, 20')
p.find_models()
print p.models
# put the last axiom back (notice that the dot is optional)
p.axioms.add('x * x = 1')
p.find_proofs()
# Show the hints
print p.hints
```
## Attributes:
### proofs
_Proofs_ instance containing all proofs found.
----
### models
_Models_ instance containing all models found.
----
### axioms
_Lines_ instance with all assumptions.
----
### goals
_Lines_ instance with the goals.
----
### hints
_Lines_ instance with hints found in all proofs.
----
### givens
_Lines_ instance with all givens found in all proofs.
----
### weights
_Lines_ instance with weights list from input.
----
### kbo\_weights
_Lines_ instance with kbo\_weights list from input.
----
### actions
_Lines_ instance with actions list from input.
----
### interps
_Lines_ instance with interpretations list from input.
----
### filename
Name of the input file.
### input
_Lines_ instance with all the lines from input.
### output
_Lines_ instance with all the lines from prover9/mace4 output.
----
## Methods:
### \_\_init\_\_(filename)
**Constructor**, filename is a string with the name/path of the input file. It can also receive a string (with embedded newlines).
----
### find\_proofs()
Tries to find a proof and returns the number of proofs found.
----
### find\_models(isofilter = False, ignore\_constants = False)
Tries to find models and returns the number of interpretations found.
It takes two boolean parameters:
- **isofilter**: will eliminate models that are isomorphic to one already found.
- **ignore\_constants** will ignore all constants during the isomorphism tests.
----
### find\_both()
This function will launch two Proverx instances simultaneously (one with prover9 and one with mace4) and will return the first one that gives an answer (a proof or a model).
Note that the result is a Proverx object.
----
### set\_option(\*args)
Sets prover9/mace4 options.
The parameter args is a list of _srings_.
The first argument should be 'Mace4' or 'Prover' (if omitted , the option will affect both cases).
Example:
```python
p.set_option('Mace4','assign','max_models, 20')
```
----
### get\_option(\*args)
Returns a prover9/mace4 option.
The parameter args is a list of _srings_.
The first argument should be 'Mace4' or 'Prover' (if omitted , the option will affect both cases).
Example:
```python
p.get_option('Prover9','assign')
```
----
### prooftrans(fname, *args)*
This function will use the utility _Prooftrans_ to create a new file **fname** with a modified view of the proof.
The parameter args is a list of Prooftrans options:
- **renumber:** renumber the steps of each proof consecutively, starting with step 1.
- **parents\_only:** list only the parents in the justifications, not the details about inference rules or positions.
- **striplabels:** tells Prooftrans to remove all label attributes on clauses.
- **expand** tells Prooftrans to produce more detailed proofs.
- **xml** or **XML** tell Prooftrans to produce proofs in XML.
- **ivy** or **IVY** tell Prooftrans to produce very detailed proofs that can be checked with the Ivy proof checker.
- **hints** tells Prooftrans to take all of the proofs in the file and produce one list of hints that can be given to Prover9 to guide subsequent searches on related conjectures.
For instance, this instruction will create a file called 'proof.txt' with all the clauses renumbered.
```python
p.prooftrans('proof.txt','renumber')
```
----
# Class Preprocessor
This class is automatically called by Proverx on initialisation. it will preprocess the input file and will create a new file with the same name and extension '.tmp' with pure prover9 syntax. Proverx will then parse this file.
## New directives:
The preprocessor allows to add some new directives to prover9:
### Include
This directive allows to include another file.
For instance:
```python
include(preferences).
```
will include an external file called 'preferences' that can contain some common options. If the file is not found in your local folder, it will search it on your local include folder, lastly, if still not found, it will search the include folder on the server (for example, in this particular case there is a file called preferences that contains some common prover9 and mace4 options).
Another use is to include known theories like so:
```python
include(group)
```
This will include a file called ‘group’ that contains the base axioms of a group.
### Exponentiation
The \*\* operator can be used for exponentiation (this will also works for +,\,/,v,^ and @ symbols).
For instance:
```python
x ** 3 = 1.
```
Translates to:
```python
(x * x) * x = 1.
```
### For loops
You can can create long lists of axioms using for loops.
For example:
```python
for(n,2,5).
x ** n = n.
(y + z) ** n = 0.
end_for.
```
will be translated to:
```python
x * x = 2.
(y + z) * (y + z) = 0.
(x * x) * x = 3.
((y + z) * (y + z)) * (y + z) = 0.
((x * x) * x) * x = 4.
(((y + z) * (y + z)) * (y + z)) * (y + z) = 0.
(((x * x) * x) * x) * x = 5.
((((y + z) * (y + z)) * (y + z)) * (y + z)) * (y + z) = 0.
```
### Define functions by induction
For example, if you define two functions:
```python
induction(f).
f(0) = (x * y).
f(n) = f(n-1) * (x**n).
end_induction.
induction(fn, k)
% main func
fn(k) = fn(k-1) + fn(k-2).
% base cases
fn(1) = y.
fn(0) = x.
end_induction
```
then, the line:
```python
f(2) = fn(3).
```
will be translated to:
```python
(((x * y) * (x * x)) * (x * x)) = ((y + x) + y).
```
Notice that induction can take an optional second parameter with the name of the variable (n by default).
----
# Class Lines
Lines is a utility class for handling text lines. It is used by axioms, goals, givens, etc.
It subclasses list and adds methods for saving and opening text files, set methods (union, intersection etc.) and a very useful method to generate all subsets.
It can also backup itself (create an internal copy) and restore.
usage:
```python
l = Lines()
l.add('Line two')
l.add('Line two')
l.save('example.txt')
```
## Methods:
### Lines.\_\_init\_\_(lines)
**Constructor**: _lines_ can be a list of text lines or any other type (it's _str_ representation will be stored).
----
### Lines.add\_first(line)
Inserts _line_ at the beginning.
----
### Lines.add\_last(line)
Appends _line_ to the end.
----
### Lines.add(lines)
Adds one or more lines (_lines_ can be a list).
----
### Lines.remove\_first()
Removes the first line.
----
### Lines.remove\_last()
Removes the last line.
----
### Lines.clear()
Clears the list.
----
### Lines.replace(lines)
This method is used (and preferred) instead of the usual assignment. It clears the list and add the new lines
----
### Lines.backup()
Creates a copy of its internal list.
----
### Lines.restore()
Restores the internal list to the one stored by backup.
----
### Lines.save(fname)
Saves the list to file _fname_.
----
### Lines.open(fname)
Opens a file of text lines and stores them in the internal list.
----
### Lines.save\_as\_list(fname, list\_name)
Saves the list to file _fname_ but inserts "formulas(_list\_name_)." at the beginning and appends "end\_of\_list." at the end. (This is useful, for example, to export hints).
----
### Lines.open\_from\_list(fname)
Opens a text file contains a list definition (starting by "formulas" and ending by "end\_of\_list.") and removes the first and last line before storing the remaining lines.
----
### Lines.union(lines)
Returns the union of _lines_ with the internal list (identical lines are not duplicated).
----
### Lines.intesection(lines)
Returns the intersection of _lines_ with the internal list.
----
### Lines.difference(lines)
Returns the difference (as a set) of _lines_ with the internal list.
----
### Lines.symmetric\_difference(lines)
Returns the symmetric difference (as a set) of _lines_ with the internal list.
----
### Lines.update(lines)
Adds only the _lines_ that are not already stored in the internal list.
----
### Lines.issameset(lines)
Tests if _lines_ and the internal list are the same set.
----
### Lines.isdisjoint(lines)
Tests if _lines_ and the internal list are disjoint.
----
### Lines.issubset(lines)
Tests if _lines_ is a subset of the internal list.
----
### Lines.issuperset(lines)
Tests if _lines_ is a superset of the internal list
----
### Lines.superset\_in(base)
Tests if the subset formed by the internal list is a superset of one of the sets of _base_.
----
### Lines.subset\_in(base)
Tests if the subset formed by the internal list is a subset of one of the sets of _base_.
----
### Lines.is\_in(base)
Tests if the subset formed by the internal list is equal to one of the sets of _base_.
----
### Lines.subsets(max\_size = -1, order = 'asc', keep\_empty = True)
Returns all subsets of maximum size _max\_size_ from the internal list. If _max\_size_ is -1, then it returns all subsets (this is the default)). It can be ordered (_order_ = 'asc' or 'desc') by the size of the subsets (by default it gives the smallest subsets first). Furthermore, if _keep\_empty_ is true, it will also return the empty set (by default).
----
# Module proofs
## Class Proofs
This class acts as an array of proofs. It has an _str_ representation similar to the one give by prover9, so it is very easy to see all profs on screen (just use print).
Example:
```python
p = Proverx('abelian.in')
p.find_proofs()
print p.proofs[0].stats.max_weight
```
This will give you the maximum weight of the first proof found (remember that indexes starts at 0 in python).
### Attributes:
#### count
**int** : the number of proofs.
----
#### found
**boolean** : indicates if at least one proof was found.
----
#### hints
**Lines** : a list of hints from all the proofs.
----
#### stats
**ProofsStats** : statistics about the proofs (see ProofsStats class).
\----
## Class Proof
This class encapsulates one proof. It acts as an ordered dict of clauses (see ProofClause class) indexed by the id of the clause.
### Attributes:
#### hints
**Lines** : a list of hints extracted from the proof.
----
#### stats
**ProofStats** : statistics about the proofs (see ProofStats class).
\----
## Class ProofClause
This corresponds to a clause from the proof.
### Attributes:
#### id (string)
#### literals (string)
#### attributes (string)
#### justifications (string)
----
## Class GivenClause
This class encapsulates _given_ clauses.
### Attributes:
#### sequence (string)
#### pick (string)
#### weight (string)
#### id (string)
#### literals (string)
#### attributes (string)
#### justifications (string)
----
## Class ProofStat
This class gives statistic informations about each proof.
### Attributes:
#### number (int)
#### seconds (float)
#### label (string)
#### length (int)
#### level (int)
#### max\_weight (float)
#### given (int)
----
## Class ProofStats
This class gives statistic informations about all the proofs.
### Attributes:
#### given (int)
#### generated (int)
#### kept (int)
#### proofs = (int)
#### usable = (int)
#### sos = (int)
#### demods = (int)
#### megs = (float)
#### time = (float)
----
# Module models
## Class Models
This class acts as an array of interpretations. It has an _str_ representation similar to the one give by mace4, so it is very easy to see all models on screen (just use print).
### Attributes:
#### count
**int** : the number of interpretations.
----
#### found
**boolean** : indicates if at least one interpretation was found.
----
### Methods:
#### save(fname, format = 'standard', wrap = False)
Saves the interpretations found with one of the formats used by the utility _interpformat_:
- **standard**: This transformation simply extracts the structure from the file and reprints it in the same (standard) format, with one line for each operation. The result should be acceptable to any of the LADR programs that take standard structures.
- **standard2**: This is similar to standard, except that the binary operations are split across multiple lines to make them more human-readable. The result should be acceptable to any of the LADR programs that take standard structures.
- **portable**: This form is a lists of strings and natural numbers. It can be parsed by several scripting systems such as GAP, Python, and Javascript.
- **tabular**: This form is designed to be easily readable by humans. It is not meant for input to other programs.
- **raw**: This form is a sequence of natural numbers.
- **cooked**: This form is a sequence of ground terms.
- **xml**: This is an XML form.
- **tex**: This generates LaTeX source for the interpretation.
If the optional wrap parameter is true, the items of the list will be wrapped in "list(interpretations)." and "end\_of\_list.".
----
## Class Interp
This class implements each interpretation found in class models.
### Attributes:
#### functions
An OrderedDict indexed by the name of the function (or constant) containing the matrix of the interpretation.
For example:
```python
p = Proverx('abelian.in')
p.axioms.pop()
p.find_models()
print p.models[0].functions
```
will return:
```python
OrderedDict([('c1', [0]), ('c2', [2]), ("'", [0, 1, 2, 4, 3, 5]), ('*', [1, 0, 3, 2, 5, 4, 0, 1, 2, 3, 4, 5, 4, 2, 1, 5, 0, 3, 5, 3, 0, 4, 1, 2, 2, 4, 5, 1, 3, 0, 3, 5, 4, 0, 2, 1])])
```
and
```python
print p.models[0]['*']
```
will return:
```html
[1, 0, 3, 2, 5, 4, 0, 1, 2, 3, 4, 5, 4, 2, 1, 5, 0, 3, 5, 3, 0, 4, 1, 2, 2, 4, 5, 1, 3, 0, 3, 5, 4, 0, 2, 1]
```
----
#### arity
An OrderedDict indexed by the name of the function (or constant) containing the arity of each function (or 0 for the constants).
For example:
```python
p = Proverx('abelian.in')
p.axioms.pop()
p.find_models()
print p.models[0].arity
```
will return:
```python
OrderedDict([('c1', 0), ('c2', 0), ("'", 1), ('*', 2)])
```
----
#### size
The size of the interpretation.
----
#### number
The number of the interpretation.
----
#### seconds
The seconds to find the interpretation.
----
### Methods:
#### matrix(function, increment = 0)
Returns a matrix (a list of lists) from the desired function and optionally increments every element by some integer.
This can be useful to pass models to [gap][1].
For instance:
```python
print p.models[0].matrix('*', 1)
```
will return:
```html
[[2, 1, 4, 3, 6, 5], [1, 2, 3, 4, 5, 6], [5, 3, 2, 6, 1, 4], [6, 4, 1, 5, 2, 3], [3, 5, 6, 2, 4, 1], [4, 6, 5, 1, 3, 2]]
```
----
# Class Parallel
This class allows to run several prover9/mace4 jobs in parallel. This class is used internally by Proverx class for its **find\_both()** method.
## Attributes:
### proc
This is a proverX object (the one that succeeded).
----
### type
Type of answer ('Prover9' or 'Mace4').
----
### proofs
Number of proofs found (in case type is 'Prover9').
----
### models
Number of models found (in case type is 'Mace4').
----
## Methods:
### add(proc, proc\_type, label = '')\\\_
Adds a Proverx object to it's internal list with the type of what we want to find (options are: 'Prover9' or 'Mace4') and an optional label to identify the answer given by **run**().
----
### run(wait = .5)
Runs all Proverx objects in it's internal list (either **find\_proofs()** or **find\_models()** depending on the type).
Every **wait** seconds it checks if a model or a proof was found. If so, it will kill the others and return a string indicating what was found.
----
Example:
```python
p1 = Proverx('abelian.in')
p2 = Proverx('abelian.in')
p3 = Proverx('abelian.in')
p4 = Proverx('abelian.in')
p5 = Proverx('abelian.in')
c = Parallel()
c.add(p1, 'Mace4', 'label mace 1 - 60 secs' )
p2.set_option('Mace4','assign','max_seconds, 5')
c.add(p2, 'Mace4', 'label mace 2 - 5 secs' )
p3.set_option('Mace4','assign','max_seconds, 10')
c.add(p3, 'Mace4', 'label mace 3 - 10 secs' )
p4.set_option('Mace4','assign','max_seconds, 15')
p4.axioms.pop()
c.add(p4, 'Mace4', 'label mace 4 - 15 secs' )
p5.set_option('Mace4','assign','max_seconds, 20')
c.add(p5, 'Mace4', 'label mace 5 - 20 secs' )
print c.run()
print "Proofs = {}".format(c.proofs)
print "Models = {}".format(c.models)
print c.type
if c.proc:
print c.proc.label
```
Answer:
```bash
Found 1 interp(s).
Proofs = 0
Models = 1
None
label mace 4 - 15 secs
```
This code creates five Proverx objects initialised with file abelian.in (for which mace4 cannot find a proof). Each one will have a different option for max\_seconds (so it will run that amount of time). They arre all added to Parallel (with a label to know who is who) but the last axiom is removed from p4, thus allowing mace4 to find a model.
----
# Module Strategies
This module is a collection of methods that implements various strategies for attacking complex proofs, finding shorter proofs, optimising parameters, etc.
## Methods:
### create\_all\_options(\*options)
Given a list of options, it will create all possible combinations. There are two types of options: assign and set/clear. The assign options are a tuple with the first element designating the name of the option and the second is a list with all possible options. For set/clear, just enter a string with the name of the option.
Example:
```python
all_options = create_all_options(('order', ['kbo', 'rpo', 'lpo']), 'factor')
for opt in all_options:
print opt
```
Answer:
```python
(['assign', 'order, kbo'], ['set', 'factor'])
(['assign', 'order, kbo'], ['clear', 'factor'])
(['assign', 'order, rpo'], ['set', 'factor'])
(['assign', 'order, rpo'], ['clear', 'factor'])
(['assign', 'order, lpo'], ['set', 'factor'])
(['assign', 'order, lpo'], ['clear', 'factor'])
```
----
### find\_best\_options(fname , proof, stat, \*options)
This function will open the file **fname** and will try to find the best set of **options** that optimizes **stat** (typically it will be 'length' to try to find the shortest proof). Proof will be the number of the proof to optimize (usually 0).
The parameter stat can be: length, seconds, max\_weight, level or given. It can also be 'first' in which case all the options will run in parallel and the fastest one will be returned.
The function returns the minimum value found and the set of options.
Example:
```python
print find_best_options('hard.in', 2, 'length', ('order', ['kbo', 'rpo', 'lpo']))
```
----
### prove\_with\_goals(fname)
This function will open the file **fname** which should have several goals. It will then move all the goals except one to the assumptions and try to find a proof. If it does, it will add the hints from that proof and will remove one of the goals from the assumptions, and so on until it can prove that goal with the original axioms. It will then start all over again with another axiom.
The function returns a list of the proofs found.
Example:
```python
proofs = prove_with_goals('McKenzie.in')
```
----
### prove\_with\_interps(fname, time\_out = 5)
This function will try to find models in all subsets of the axioms in order to eliminate certain assumptions and accelerate the process of finding a proof. If it finds a model, it will add it to the interpretation list of the original theory and will try to prove it. Both prover9 and mace4 will be given a max\_seconds equal to the parameter **time\_out** (the default is 5 seconds).
It returns a ProverX object if it finds a proof or None if not.
Example:
```python
p = prove_with_interps('LT-82-2.in')
```
----
### find\_independent\_axioms(fname, time\_out = 5)
This function takes a file with a set of assumptions and will try to find all sets of independent axioms.
Example:
```python
for f in find_independent_axioms('D.in', 1):
print f
```
----
### find\_short\_proof(fname, proof, global\_time\_out = 300)
This function tries to find the shortest proof by fiddling several parameters ('order', 'back\_demod', 'and max\_weight').
If after a period of **time\_out** seconds it has not exhausted all possibilities, it will stop and return the shortest proof found until then.
Example:
```python
p = find_short_proof('hard.in', 2, time_out = 30)
```
----
### find\_enumerating\_axioms(fname, fixed\_head, fixed\_tail = 0, time\_out = 5, hints = True)
This function will open the file **fname** and will fix a certain number of axioms at the beginning and at the end (**fixed\_head** and **fixed\_tail**). It will then pick each of the remaining axioms one by one and will try to find a proof. If it does, it will add the hints from that proof before trying with the second axiom.
Example:
```python
p = find_enumerating_axioms("epivar.in", 13, 1, 300, True)
```
----
### find\_with\_axioms\_subsets(fname, fixed\_head, fixed\_tail = 0, time\_out = 5, hints = True)
This function works similarly to **find\_enumerating\_axioms()** but instead of trying the remaining axioms one by one, it will try to find a proof for all the subsets of those axioms.
Example:
```python
p = find_with_axioms_subsets("epivar.in", 13, 1, 300, True)
```
# Module extprog
This module allows to run external programs and interact with them.
## Public Methods:
### which(program)
Returns the path where **program** is installed (replicate the bash command _which_).
----
## Class Exec
This class executes an external program and interacts with its stdin, stdout streams, check if it's still running, kills it, etc.
### Public Methods:
#### \_\_init\_\_(prog\_name, parameters = [], keep\_alive = False):
**Constructor**, **prog\_name** is the path of the program, parameters can be passed through the **parameters** list.
If **keep|\_alive** is true, the program keeps running in the background.
----
#### get(timeout = 5)
Returns the last output from the running program. If after **timeout** seconds there is no response, the function returns (default 5 seconds).
----
#### command(cmd, timeout = .1)
Function that sends **cmd** to the running program and returns the output.
----
#### kill()
Sends a kill signal to the running program.
----
#### terminate()
Sends a terminate signal to the running program.
----
#### close()
Closes the running program.
----
#### poll()
Returns the return code of the running program if it has finished running or None otherwise.
----
#### retcode()
The same as poll.
----
#### running()
Returns true if the program is still running.
----
#### set\_quit\_cmd(quit\_cmd)
Sets the command used for closing the running program. (for instance 'quit;' in GAP). If no command is provided, the program is just killed.
----
## Class Gap
This class is a subclass of Exec. It creates an instance of GAP and interacts with it by sending commands.
```bash
>g = Gap()
>g('S4:=SymmetricGroup(4)')
'Sym( [ 1 .. 4 ] )'
```
----
## Class Race
This class creates a list of programs and executes them in parallel. If one of the programs finishes first, all the others will be killed. The output (and eventual error message) from the first program is kept.
### Instance variables:
#### progs
List of running programs.
----
#### output
String with the output from the first program that finished.
----
#### error
String with the error output from the first program that finished.
----
### Public Methods:
#### \_\_init\_\_(progs)
**Constructor**, accepts a list of paths:
----
#### add(prog)
Adds a program path to the list of programs.
----
#### run(interval = 1)
Executes the list of programs concurrently. It checks if a program has finished every **interval** seconds (default is one second, this value can be a float).
----
# Extending ProverX
ProverX can be easily extended by writing python modules. These modules can be installed on the **system** folder (reserved for ProverX), the **lib folder** (for all third party extensions) or the **user** folder.
## Writing packages
A package can be a simple python function or a class. It can also be an external program or programs (or even a web API) but, in this case, there must be a python module acting as an interface. To access ProverX functionality, the module should always start by importing proverx (see example below).
## An example
Here is an example of an extension that draws a directed graph of the proof (see Quick Start):
Create a file called proofgraph.py
```python
import re
import graphviz
import proverx
class ProofGraph(object):
def __init__(self, proof = None, filename='graph'):
self.graph = graphviz.Digraph(format='png', filename = filename + '.gv')
self.graph.node('$F',shape='doublecircle')
for id, clause in proof.clauses.iteritems():
depends = self.depends_from(clause.justifications)
if depends:
for dep_id in depends:
self.graph.edge(proof.clauses[dep_id].literals, proof.clauses[id].literals)
def depends_from(self, clause):
ids = []
rewrites = re.findall(r"rewrite\(\[.*?\]\)", clause, re.I) #find rewrite justifications
for rewrite in rewrites:
ids += re.findall(r"([0-9]+[A-Z]*)\(", rewrite, re.I) #get clauses ids from rewrite
clause = clause.replace(rewrite, '')
paras = re.findall(r"para\(.*?\)\)", clause, re.I) #find para justifications
for para in paras:
ids += re.findall(r"([0-9]+[A-Z]*)\(", para, re.I) #get clauses ids from para
clause = clause.replace(para, '')
ids += re.findall('[0-9]+[A-Z]*', clause, re.I) # get remaining ids
return list(set(ids)) #remove duplicate ids
def create_graph(self):
self.graph.render()
```
Once installed this extension can be used like so:
```python
from proofgraph import *
pg = ProofGraph(p.proofs[0], 'abelian')
pg.create_graph()
```
[1]: https://www.gap-system.org