Commit 8944f834 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Add a second example of resolution proof.

This is the smallest proof produced by prover9 that uses both rules of resolution.
parent 2387337b
#NAME NUM343_1.
def type := fol.type.
def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
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.
def 2 := nat.S 1.
(; Signature ;)
A : type.
LEQ : predicate.
[] fol.pred_arity LEQ --> read_types 2 A A.
N : function.
[] fol.fun_arity N --> nil_type.
[] fol.fun_codomain N --> A.
def leq : term A -> term A -> prop := pred_apply LEQ.
def n : term A := fun_apply N.
(; Axioms ;)
def A0 := all A (x => all A (y => or (leq x y) (leq y x))).
a0 : proof A0.
def A1 := all A (x => not (leq x n)).
a1 : proof A1.
(; Clauses ;)
def C0 := resolution.qclause_of_prop A0.
thm c0 : resolution.qcproof C0 := resolution.qclause_of_prop_correct A0 a0.
def C1 := resolution.qclause_of_prop A1.
thm c1 : resolution.qcproof C1 := resolution.qclause_of_prop_correct A1 a1.
def C2' := resolution.factor 0 1 C0.
thm c2' : resolution.qcproof C2' := resolution.factor_correct 0 1 C0 c0.
def C2 := resolution.unquantify C2'.
thm c2 : resolution.qcproof C2 := resolution.unquantify_correct C2' c2'.
def C3' := resolution.resolve 0 0 C1 C2.
thm c3' : resolution.qcproof C3' := resolution.resolve_correct 0 0 C1 C2 c1 c2.
def C3 := resolution.unquantify C3'.
thm c3 : resolution.qcproof C3 := resolution.unquantify_correct C3' c3'.
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