Commit 96747e72 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Description of the resolution module

parent 3efe270e
......@@ -7,6 +7,50 @@
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;)
(; This module defines tactics corresponding to resolution certificates.
The resolution calculus is a proof calculus for showing the
inconsistency of a conjunction of clauses. The calculus contains
only two rules (on implicitely quantified clauses modulo AC for ∨):
C₁ ∨ l₁ C₂ ∨ ¬l₂ σ = mgu(l₁, l₂)
——————————————————–——————————————————– Resolution
(C₁ ∨ C₂)σ
C ∨ l₁ ∨ l₂ σ = mgu(l₁, l₂)
—————————————————————————————– Factorisation
(C ∨ l₁)σ
The choice of the most general unifier is here to ensure
completeness of the calculus. In our case, we are only interested
in its correctness so if the substitution is provided in the
certificate, we do not need to check it is actually the most
general. Moreover, we can further decompose the rules to simplify
them:
C
————–— Instantiation
C₁ ∨ l C₂ ∨ ¬l
————————————————— Propositional resolution
C₁ ∨ C₂
C ∨ l ∨ l
————————– Propositional factorisation
C ∨ l
The Otter prover for example is able to give this level of detail
;)
def prop := fol.prop.
def proof := fol.proof.
def not := fol.not.
......@@ -38,6 +82,14 @@ def resolution (C1 : prop) (C2 : prop)
(Hl => fol.false_elim (or C1 C2) (Hnl Hl))).
(; goal is a disjunction containing A, a proof of A is in context ;)
(; Reasoning modulo AC for ∨ ;)
(; We define a certificate for C₁ ⊢ C₂ when C₁ =_AC C₂ ;)
(; In fact it is even a bit more powerful since it only requires C₂ ⊂
C₁ (set inclusion). ;)
(; Remark: this is highly non deterministic and can thus be slow; to speed up,
we could take as argument a mapping from the disjuncts of C₂ to the one of C₁ ;)
(; Proves Aₖ |- A₁ ∨ … ∨ Aₙ ;)
def modulo_ac_base : certificate
:=
cert.repeat (t =>
......@@ -48,6 +100,9 @@ def modulo_ac_base : certificate
(; A and Goal are disjunctions such that each part of A appears in Goal.
A is an assumption. ;)
(; We apply all possible ∨-left rules on one non-deterministically
chosen assumption and then modulo_ac_base. ;)
def modulo_ac : certificate :=
cert.repeat (mac =>
cert.with_assumption (A => a =>
......@@ -55,6 +110,7 @@ def modulo_ac : certificate :=
(A1 => A2 =>
cert.destruct_or A1 A2
(cert.exact A a)
(; clear A = A₁∨A₂ to avoid looping ;)
(cert.intro (cert.clear A mac))
(cert.intro (cert.clear A mac)))
modulo_ac_base)).
......@@ -106,7 +162,7 @@ def qclause_to_prop : qclause -> prop.
def prop_to_qclause_to_prop : A : prop -> proof A -> proof (qclause_to_prop (prop_to_qclause A)).
[] prop_to_qclause_to_prop (fol
(; [] prop_to_qclause_to_prop (fol ;)
(; a quantified biclause is a universally quantified pair of clauses.
The important fact is that the universal quantification is above
......
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