Plans regarding handling of resolution proofs.
More...
Go to the source code of this file.
Detailed Description
Plans regarding handling of resolution proofs.
 Todo:
 php_ext_resl

php_ext_resl defines the resolution proof of the extension of the pigeonhole formulas as discussed by Cook in [A short proof of the pigeon hole principle using extended resolution"; Stephen Cook].

We need the following for this function:

A full specification, including:

the order resolvents are generated in the proof;

the precise number of resolvents the proof for all n;

the proof given in full detail in the docus (transferred from Annotations).

Tests.

Resolution lists:

The function currently defines the resolution proof as a list of clauses and "resolvents", where the resolvents are pairs [C,[C1,C2]] where C, C1 and C2 are clauses.

This list is then converted to a "resolution list" by mapping the clauses C1 and C2 to their (smaller) index in the list.

Using clauses rather than indices for the parents of the resolvent is much more readable when writing the generators for such proofs.

We should define another type to encompass this "raw" resolution list, and a conversion function.

We should also have a type which just specifies a list of clauses generated (in the order of the list), and then a function which converts this to a resolution list assuming a resolvent was generated by resolving the first two possible parents.
 Todo:
 Resolution trees

Function st2reslrt_cs in ComputerAlgebra/Satisfiability/Lisp/Backtracking/SplittingTrees.mac transforms splitting trees into resolution trees.

There is also a function for outputting resolution trees; this function should move here.

We need to make this concept explicit.

A "resolution tree" ("reslrt"; for the boolean case) is a rooted binary tree labelled with clauses such that each inner nodelabel is the resolvent of the labels of the two children.

We can represent such a labelled rooted binary tree in Maxima using our notion of a labelled rooted tree, given in ComputerAlgebra/Trees/Lisp/Basics.mac.

When translating a resldg (see below) into a reslrt, then we loose the vertex labels. In order to represent them, one needed rooted trees where the labels are pairs, the clause and the original label.

Such "labelled resolution trees" ("resllrt", for 2 labels) should also be useful.

We will also have collections (at least sets) of resolution trees; one might introduce the notion of a "resolution forest".
 Todo:
 Resolution proofs

The natural format for a resolution proof is a nonempty list, where each entry is either a clause (an "axiom") or a pair consisting of a clause (the "resolvent") and a pair of (smaller) indices (the indices of the "parent clauses").

Resolution proofs as digraphs:

The graph notions are defined in ComputerAlgebra/Graphs/Lisp/Basic.mac.

A "resolution proof as directed graph" ("resdg") is a dg [V,E] such that

V is a set of clauses

For every edge [C,D] in E, there is another edge [C,D'] such that D and D' resolve to C.
We have that:

every resolvent points to its two parent clauses;

every sink node in the graph is an axiom;

all vertices have outdegree 0 or >= 2 (not 1).

A "resolution proof as labelled directed graph" ("resldg") is a labelled dg [[V,E],f] such that:

f maps V to clauses

for every edge [u,v] in E, there is another edge [u,v'] such that f(v) and f(v') resolve to f(u)

every node has outdegree 0 or 2.

The notion of "(vertex)labelled graph" needs to be made explicit and implemented at the Maxima level, as discussed in "Representing edge
and vertex labellings" in ComputerAlgebra/Graphs/Lisp/plans/Basic.hpp.

We need a correctnesschecker for each different form.

We need functions to translate between each of the different forms of resolution proofs.

We also need functions to check various properties of the proof structures. For example:

Is a proof treelike?

Is a proof regular?

Is the proof repetitionfree?

Some or all of the relevant properties of resolution proofs will be implementable directly using existing functions on the underlying representations.

Likely at first, we implement just the functions for lists and digraphs, as the notions for the underlying datastructures are already developed in the library.

Naming conventions:

We need abbreviations for the following notions:

resolution proof as a list;

resolution proof as a digraph;

resolution proof as a labelled digraph;

(tree)resolution proof as a rooted tree (discussed in "Resolution trees" above).

We use "resl","reslrt", "resdg", "resldg".

DONE (irrelevant: if one would read it as this word, it wouldn't make sense) It *is* unfortunate that "rest" is a word, as this might create confusion.

We should also investigate the existing fileformats for resolution proofs, and we should provide input and outputfacilities.

The above can easily be generalised to nonboolean clausesets.

DONE (discussed separately w.r.t labelled digraphs) This linear format is in 11 correspondence to the representation via labelled dag's; we need a representation of labelled graphs, digraphs and labelled digraphs.
 Todo:
 Readonce resolution proofs

Write a checker whether a resolution proof is readonce.

Implement the translation of "has readonce refutation" into SAT.
Definition in file Proofs.hpp.