From 96747e7275199582f096ba0398a83adc24a7ad56 Mon Sep 17 00:00:00 2001 From: Raphael Cauderlier Date: Tue, 23 Jan 2018 15:34:50 +0100 Subject: [PATCH] Description of the resolution module --- meta/resolution.dk | 58 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 57 insertions(+), 1 deletion(-) diff --git a/meta/resolution.dk b/meta/resolution.dk index abe5e66..a80e8a3 100644 --- a/meta/resolution.dk +++ b/meta/resolution.dk @@ -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σ + + 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 -- 2.24.1