Commit 44bdb84c authored by Raphael CAUDERLIER's avatar Raphael CAUDERLIER

[fix,resolution] unquantification in a separate step to avoid early substitution of variable

parent 27989ea2
......@@ -5,52 +5,62 @@ 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 and := fol.and.
def or := fol.or.
def all := fol.all.
def predicate := fol.predicate.
def function := fol.function.
def pred_apply := fol.pred_apply.
def fun_apply := fol.fun_apply.
def read_types := fol.read_types.
def nil_type := fol.nil_type.
def 0 := nat.O.
def 1 := nat.S 0.
(; Signature ;)
A : type.
P : fol.predicate.
[] fol.pred_arity P --> fol.read_types 1 A.
O : fol.function.
[] fol.fun_arity O --> fol.nil_type.
P : predicate.
[] fol.pred_arity P --> read_types 1 A.
O : function.
[] fol.fun_arity O --> nil_type.
[] fol.fun_codomain O --> A.
S : fol.function.
[] fol.fun_arity S --> fol.read_types 1 A.
S : function.
[] fol.fun_arity S --> 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 p : term A -> prop := pred_apply P.
def o : term A := fun_apply O.
def s : term A -> term A := fun_apply S.
(; Axioms ;)
def A0 := p o.
def A1 := all A (x => or (p (s x)) (not (p x))).
a0 : proof A0.
def A1 := all A (x => or (not (p x)) (p (s x))).
a1 : proof A1.
def A2 := not (p (s (s o))).
a2 : proof A2.
def a0 : proof A0.
def a1 : proof A1.
def a2 : proof A2.
(; Clauses ;)
def C0 := resolution.qclause_of_prop A0.
def c0 : resolution.qcproof C0 := resolution.qclause_of_prop_correct A0 a0.
thm 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.
thm 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 0 C0 C1.
thm c3' : resolution.qcproof C3' := resolution.resolve_correct 0 0 C0 C1 c0 c1.
def C3 := resolution.unquantify C3'.
thm c3 : resolution.qcproof C3 := resolution.unquantify_correct C3' c3'.
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.
def C4' := resolution.resolve 0 0 C3 C1.
thm c4' : resolution.qcproof C4' := resolution.resolve_correct 0 0 C3 C1 c3 c1.
def C4 := resolution.unquantify C4'.
thm c4 : resolution.qcproof C4 := resolution.unquantify_correct C4' c4'.
def C5 := resolution.resolve 0 0 C4 C1.
thm c5 : resolution.qcproof C5 := resolution.resolve_correct 0 0 C4 C1 c4 c1.
......@@ -237,14 +237,10 @@ def unquantify_correct : Q : clauses.qclause -> qcproof Q -> qcproof (unquantify
x => unquantify_correct (P x) (H x).
def factor (i : nat) (j : nat) (Q : clauses.qclause) : clauses.qclause :=
unquantify (remove_nth_q j (subst_qclause Q (unify_litterals_q i j Q))).
remove_nth_q j (subst_qclause Q (unify_litterals_q i j Q)).
def factor_correct (i : nat) (j : nat) (Q : clauses.qclause) (H : qcproof Q) : qcproof (factor i j Q) :=
(Q' : clauses.qclause =>
HQ' : qcproof Q' =>
unquantify_correct
(remove_nth_q j Q')
(remove_nth_q_correct j Q' HQ'))
remove_nth_q_correct j
(subst_qclause Q (unify_litterals_q i j Q))
(subst_qcproof Q (unify_litterals_q i j Q) H).
......@@ -323,17 +319,15 @@ def remove_ith_and_jth_correct : i : nat -> j : nat -> B : biclause -> bcproof B
def resolve (i : nat) (j : nat) (Q : clauses.qclause) (Q' : clauses.qclause) : clauses.qclause :=
(B : biclause =>
unquantify (remove_ith_and_jth i j (subst_biclause B (biclause_unify i j B))))
remove_ith_and_jth i j (subst_biclause B (biclause_unify i j B)))
(qclause_merge Q Q').
def resolve_correct (i : nat) (j : nat) (Q : clauses.qclause) (Q' : clauses.qclause)
(H : qcproof Q) (H' : qcproof Q') : qcproof (resolve i j Q Q') :=
(B : biclause =>
HB : bcproof B =>
unquantify_correct
(remove_ith_and_jth i j (subst_biclause B (biclause_unify i j B)))
(remove_ith_and_jth_correct i j (subst_biclause B (biclause_unify i j B))
(subst_bcproof B (biclause_unify i j B) HB)))
remove_ith_and_jth_correct i j (subst_biclause B (biclause_unify i j B))
(subst_bcproof B (biclause_unify i j B) HB))
(qclause_merge Q Q') (qclause_merge_correct Q Q' H H').
......
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