Proofs.hpp File Reference

Plans regarding handling of resolution proofs. More...

Go to the source code of this file.

Detailed Description

Plans regarding handling of resolution proofs.

  • php_ext_resl defines the resolution proof of the extension of the pigeon-hole 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.
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 node-label 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".
Resolution proofs
  • The natural format for a resolution proof is a non-empty 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 out-degree 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 out-degree 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 correctness-checker 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 tree-like?
    • Is a proof regular?
    • Is the proof repetition-free?
  • 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 file-formats for resolution proofs, and we should provide input- and output-facilities.
  • The above can easily be generalised to non-boolean clause-sets.
  • DONE (discussed separately w.r.t labelled digraphs) This linear format is in 1-1 correspondence to the representation via labelled dag's; we need a representation of labelled graphs, digraphs and labelled digraphs.
Read-once resolution proofs
  • Write a checker whether a resolution proof is read-once.
  • Implement the translation of "has read-once refutation" into SAT.

Definition in file Proofs.hpp.