Commit e2df7571 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Almost working checking of resolution proofs

parent c4c2eb6b
#NAME resolution_examples.
def type := fol.type.
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
def all := fol.all.
def or := fol.or.
def false := fol.false.
def not := fol.not.
def 0 := nat.O.
def 1 := nat.S 0.
A : type.
P : fol.predicate.
[] fol.pred_arity P --> fol.read_types 1 A.
O : fol.function.
[] fol.fun_arity O --> fol.nil_type.
[] fol.fun_codomain O --> A.
S : fol.function.
[] fol.fun_arity S --> fol.read_types 1 A.
[] fol.fun_codomain S --> A.
def o : term A := fol.fun_apply O.
def s : term A -> term A := fol.fun_apply S.
def p : term A -> prop := fol.pred_apply P.
def A0 := p o.
def A1 := all A (x => or (p (s x)) (not (p x))).
def A2 := not (p (s (s o))).
def a0 : proof A0.
def a1 : proof A1.
def a2 : proof A2.
def C0 := resolution.qclause_of_prop A0.
def c0 : resolution.qcproof C0 := resolution.qclause_of_prop_correct A0 a0.
def C1 := resolution.qclause_of_prop A1.
def c1 : resolution.qcproof C1 := resolution.qclause_of_prop_correct A1 a1.
def C2 := resolution.qclause_of_prop A2.
def c2 : resolution.qcproof C2 := resolution.qclause_of_prop_correct A2 a2.
def C3 := resolution.resolve 0 1 C0 C1.
#CONV C3, resolution.qclause_of_prop (p (s o)).
def c3 : resolution.qcproof C3 := resolution.resolve_correct 0 1 C0 C1 c0 c1.
def C4 := resolution.resolve 0 1 C3 C1.
#CONV C4, resolution.qclause_of_prop (p (s (s o))).
def c4 : resolution.qcproof C4 := resolution.resolve_correct 0 1 C3 C1 c3 c1.
#CONV resolution.resolve 0 0 C4 C2, clauses.qc_base clauses.empty_clause.
def c5 : proof false := resolution.resolve_correct 0 0 C4 C2 c4 c2.
......@@ -690,8 +690,8 @@ combinator) and then uses the classical lemma
*** Minimal logic
*** Presburger arithmetic
* TODO Interactive proof development
* TODO Checking output of automatic theorem provers
** Reasoning modulo AC, ACU, symmetry
* Checking output of automatic theorem provers
** TODO Reasoning modulo AC, ACU, symmetry
** Shallow substitutions and unification
......@@ -741,7 +741,7 @@ combinator) and then uses the classical lemma
- =[A,a,s,p] unif.subst_prop (unif.cons_subst A a a s) p --> unif.subst_prop s p=
- =[A,a,s,p] unif.subst_prop unif.empty_subst p --> p=
*** Rewrite rules for unification
*** Unification
A (first-order) unification problem is a list of pairs of terms
(both terms having the same type). Unification can either fail or
......@@ -762,3 +762,43 @@ combinator) and then uses the classical lemma
** Resolution
The resolution calculus is a very simple proof calculus for
classical first-order logic. It is a clausal calculus; this means
that it does not handle the full syntax of first-order formulae but
only the CNF (clausal normal form) fragment.
A *litteral* is either an atom (a positive litteral) or the
negation of an atom (a negative litteral), a *clause* is a
disjunction of litterals. Litterals and clauses may contain free
variables which are to be interpreted as universally quantified. A
*quantified clause* is an explicitly universally quantified clause.
The simplest way to define a clause is by parsing the corresponding
proposition using the partial function
=resolution.qclause_of_prop=:
- =resolution.qclause_of_prop : fol.prop -> resolution.qclause=
- =resolution.qclause_of_prop_correct : p : fol.prop -> fol.proof p -> resolution.qcproof (resolution.qclause_of_prop p)=
A resolution proof is a derivation of the empty clause
(representing falsehood) from assumed clauses using the following
two reasoning rules:
#+BEGIN_example
l₁ ∨ … ∨ lₙ σ = mgu(lᵢ, lⱼ)
—-—————————————————————————————– Factorisation
(l₁ ∨ … ∨ lⱼ₋₁ ∨ lⱼ₊₁ ∨ … ∨ lₙ)σ
l₁ ∨ … ∨ lₙ l'₁ ∨ … ∨ l'ₘ σ = mgu(lᵢ, ¬l'ⱼ)
——————————————————–—————————————————–————————–—––——————————————————— Resolution
(l₁ ∨ … ∨ lᵢ₋₁ ∨ lᵢ₊₁ ∨ … ∨ lₙ ∨ l'₁ ∨ … ∨ l'ⱼ₋₁ ∨ l'ⱼ₊₁ ∨ … ∨ l'ₘ)σ
#+END_example
These two rules are implemented by the following functions:
- =resolution.factor : Nat.nat -> Nat.nat -> resolution.qclause -> resolution.qclause=
- =resolution.factor_correct : i : Nat.nat -> j : Nat.nat -> Q : resolution.qclause -> resolution.qcproof Q -> resolution.qcproof (resolution.factor i j Q)=
- =resolution.resolve : Nat.nat -> Nat.nat -> resolution.qclause -> resolution.qclause -> resolution.qclause=
- =resolution.resolve_correct : i : Nat.nat -> j : Nat.nat -> Q : resolution.qclause -> Q' : resolution.qclause -> resolution.qcproof Q -> resolution.qcproof Q' -> resolution.qcproof (resolution.resolve i j Q Q')=
For an example of use of the =resolution= module, see the file [[./example/resolution_examples.dk][example/resolution_examples.dk]].
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment