Commit 481f3b33 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Pairs of quantified clauses

This structure is intended to be used for resolution and
paramodulation tactics. Having both clauses under the same quantifiers
allows to perform shallow unification.
parent cfccb191
......@@ -73,30 +73,56 @@ def lit_to_prop : lit -> prop.
[A] lit_to_prop (pos A) --> A
[A] lit_to_prop (neg A) --> not A.
(; A clause is a list of literals, a quantified clause is a
universally quantified clause ;)
(; A clause is a list of literals ;)
clause : Type.
nil_clause : clause.
cons_clause : lit -> clause -> clause.
qclause : Type.
base_qclause : clause -> qclause.
qqclause : A : type -> (term A -> qclause) -> qclause.
def clause_append : clause -> clause -> clause.
[C] clause_append nil_clause C --> C
[l,C1,C2] clause_append (cons_clause l C1) C2 --> cons_clause l (clause_append C1 C2).
def prop_to_clause : prop -> clause.
def clause_to_prop : clause -> prop.
[A,B] prop_to_clause (fol.or A B) --> clause_append (prop_to_clause A) (prop_to_clause B)
[A] prop_to_clause A --> cons_clause (prop_to_lit A) nil_clause.
def clause_to_prop : clause -> prop.
[] clause_to_prop nil_clause --> fol.false
[l] clause_to_prop (cons_clause l nil_clause) --> lit_to_prop l
[l,C] clause_to_prop (cons_clause l C) --> or (lit_to_prop l) (clause_to_prop C).
(; a quantified clause is a universally quantified clause ;)
qclause : Type.
base_qclause : clause -> qclause.
qqclause : A : type -> (term A -> qclause) -> qclause.
def prop_to_qclause : prop -> qclause.
[A,P] prop_to_qclause (fol.all A P) --> qqclause A (x => prop_to_qclause (P x))
[A] prop_to_qclause A --> base_qclause (prop_to_clause A).
def qclause_to_prop : qclause -> prop.
[C] qclause_to_prop (base_qclause C) --> clause_to_prop C
[A,C] qclause_to_prop (qqclause A C) --> all A (x => qclause_to_prop (C x)).
def prop_to_qclause_to_prop : A : prop -> proof A -> proof (qclause_to_prop (prop_to_qclause A)).
[] 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
both clauses simultaneously. ;)
qbclause : Type.
base_qbclause : clause -> clause -> qbclause.
qqbclause : A : type -> (term A -> qbclause) -> qbclause.
def qclauses_to_qbclause : qclause -> qclause -> qbclause.
[C1,C2] qclauses_to_qbclause (base_qclause C1) (base_qclause C2) --> base_qbclause C1 C2
[A,C1,C2] qclauses_to_qbclause (base_qclause C1) (qqclause A C2) --> qqbclause A (x => qclauses_to_qbclause (base_qclause C1) (C2 x))
[A,C1,C2] qclauses_to_qbclause (qqclause A C1) C2 --> qqbclause A (x => qclauses_to_qbclause (C1 x) C2).
def props_to_qbclause (A : prop) (B: prop) : qbclause :=
qclauses_to_qbclause (prop_to_qclause A) (prop_to_qclause B).
no_resolution_candidate : tac.exc.
......
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