Commit 75dd3560 authored by Raphael Cauderlier's avatar Raphael Cauderlier

fix a typo in the word "literal"

parent f255878e
...@@ -3,13 +3,13 @@ ...@@ -3,13 +3,13 @@
atom : Type. atom : Type.
mk_atom : p : fol.predicate -> fol.terms (fol.pred_domain p) -> atom. mk_atom : p : fol.predicate -> fol.terms (fol.pred_domain p) -> atom.
litteral : Type. literal : Type.
pos_lit : atom -> litteral. pos_lit : atom -> literal.
neg_lit : atom -> litteral. neg_lit : atom -> literal.
clause : Type. clause : Type.
empty_clause : clause. empty_clause : clause.
cons_clause : litteral -> clause -> clause. cons_clause : literal -> clause -> clause.
qclause : Type. qclause : Type.
qc_base : clause -> qclause. qc_base : clause -> qclause.
......
...@@ -764,13 +764,13 @@ combinator) and then uses the classical lemma ...@@ -764,13 +764,13 @@ combinator) and then uses the classical lemma
that it does not handle the full syntax of first-order formulae but that it does not handle the full syntax of first-order formulae but
only the CNF (clausal normal form) fragment. only the CNF (clausal normal form) fragment.
A *litteral* is either an atom (a positive litteral) or the A *literal* is either an atom (a positive literal) or the
negation of an atom (a negative litteral), a *clause* is a negation of an atom (a negative literal), a *clause* is a
disjunction of litterals. Litterals and clauses may contain free disjunction of literals. Literals and clauses may contain free
variables which are to be interpreted as universally quantified. A variables which are to be interpreted as universally quantified. A
*quantified clause* is an explicitly universally quantified clause. *quantified clause* is an explicitly universally quantified clause.
The types for atoms, litterals, clauses, and quantified clauses are The types for atoms, literals, clauses, and quantified clauses are
declared with their constructors in [[./fol/clauses.dk][fol/clauses.dk]]. However, the declared with their constructors in [[./fol/clauses.dk][fol/clauses.dk]]. However, the
simplest way to define a clause is by parsing the corresponding simplest way to define a clause is by parsing the corresponding
proposition using the partial function proposition using the partial function
......
...@@ -61,23 +61,23 @@ def unify_atoms_pb : clauses.atom -> clauses.atom -> unif.unify_problem. ...@@ -61,23 +61,23 @@ def unify_atoms_pb : clauses.atom -> clauses.atom -> unif.unify_problem.
def unify_atoms (a : clauses.atom) (a' : clauses.atom) : subst := def unify_atoms (a : clauses.atom) (a' : clauses.atom) : subst :=
get_subst (unif.unify' (unify_atoms_pb a a')). get_subst (unif.unify' (unify_atoms_pb a a')).
(; a positive litteral is an atom, a negative litteral is the negation (; a positive literal is an atom, a negative literal is the negation
of an atom. ;) of an atom. ;)
def lprop : clauses.litteral -> prop. def lprop : clauses.literal -> prop.
[a] lprop (clauses.pos_lit a) --> aprop a [a] lprop (clauses.pos_lit a) --> aprop a
[a] lprop (clauses.neg_lit a) --> not (aprop a). [a] lprop (clauses.neg_lit a) --> not (aprop a).
def lproof (l : clauses.litteral) := proof (lprop l). def lproof (l : clauses.literal) := proof (lprop l).
def unify_litterals : clauses.litteral -> clauses.litteral -> subst. def unify_literals : clauses.literal -> clauses.literal -> subst.
[a,a'] unify_litterals (clauses.pos_lit a) (clauses.pos_lit a') --> unify_atoms a a' [a,a'] unify_literals (clauses.pos_lit a) (clauses.pos_lit a') --> unify_atoms a a'
[a,a'] unify_litterals (clauses.neg_lit a) (clauses.neg_lit a') --> unify_atoms a a'. [a,a'] unify_literals (clauses.neg_lit a) (clauses.neg_lit a') --> unify_atoms a a'.
def unify_opposite_litterals : clauses.litteral -> clauses.litteral -> subst. def unify_opposite_literals : clauses.literal -> clauses.literal -> subst.
[a,a'] unify_opposite_litterals (clauses.pos_lit a) (clauses.neg_lit a') --> unify_atoms a a' [a,a'] unify_opposite_literals (clauses.pos_lit a) (clauses.neg_lit a') --> unify_atoms a a'
[a,a'] unify_opposite_litterals (clauses.neg_lit a) (clauses.pos_lit a') --> unify_atoms a a'. [a,a'] unify_opposite_literals (clauses.neg_lit a) (clauses.pos_lit a') --> unify_atoms a a'.
(; a clause is a list of litterals (interpreted as their disjuction) ;) (; a clause is a list of literals (interpreted as their disjuction) ;)
def cprop : clauses.clause -> prop. def cprop : clauses.clause -> prop.
[] cprop clauses.empty_clause --> false [] cprop clauses.empty_clause --> false
...@@ -85,7 +85,7 @@ def cprop : clauses.clause -> prop. ...@@ -85,7 +85,7 @@ def cprop : clauses.clause -> prop.
def cproof (C : clauses.clause) := proof (cprop C). def cproof (C : clauses.clause) := proof (cprop C).
(; /!\ nth_lit n C does not fully reduce if n ≥ lenght(C) ;) (; /!\ nth_lit n C does not fully reduce if n ≥ lenght(C) ;)
def nth_lit : nat -> clauses.clause -> clauses.litteral. def nth_lit : nat -> clauses.clause -> clauses.literal.
[l] nth_lit nat.O (clauses.cons_clause l _) --> l [l] nth_lit nat.O (clauses.cons_clause l _) --> l
[n,C] nth_lit (nat.S n) (clauses.cons_clause _ C) --> nth_lit n C. [n,C] nth_lit (nat.S n) (clauses.cons_clause _ C) --> nth_lit n C.
...@@ -129,20 +129,20 @@ def clause_append_correct : C : clauses.clause -> D : clauses.clause -> proof (o ...@@ -129,20 +129,20 @@ def clause_append_correct : C : clauses.clause -> D : clauses.clause -> proof (o
(HD => or_intro_2 (lprop l) (cprop (clause_append C D)) (HD => or_intro_2 (lprop l) (cprop (clause_append C D))
(clause_append_correct C D (or_intro_2 (cprop C) (cprop D) HD))). (clause_append_correct C D (or_intro_2 (cprop C) (cprop D) HD))).
(; /!\ very partial function, reduces only if l and l' are opposite litterals ;) (; /!\ very partial function, reduces only if l and l' are opposite literals ;)
def magic_imp : l : clauses.litteral -> l' : clauses.litteral -> lproof l -> lproof l' -> proof false. def magic_imp : l : clauses.literal -> l' : clauses.literal -> lproof l -> lproof l' -> proof false.
[a,H,H'] magic_imp (clauses.pos_lit a) (clauses.neg_lit a) H H' --> fol.imp_elim (aprop a) false H' H [a,H,H'] magic_imp (clauses.pos_lit a) (clauses.neg_lit a) H H' --> fol.imp_elim (aprop a) false H' H
[a,H,H'] magic_imp (clauses.neg_lit a) (clauses.pos_lit a) H H' --> fol.imp_elim (aprop a) false H H'. [a,H,H'] magic_imp (clauses.neg_lit a) (clauses.pos_lit a) H H' --> fol.imp_elim (aprop a) false H H'.
(; /!\ magic_or_imp l C H only reduces if l ∈ C ;) (; /!\ magic_or_imp l C H only reduces if l ∈ C ;)
def magic_or_imp : l : clauses.litteral -> C : clauses.clause -> lproof l -> cproof C. def magic_or_imp : l : clauses.literal -> C : clauses.clause -> lproof l -> cproof C.
[l,C] magic_or_imp l (clauses.cons_clause l C) --> [l,C] magic_or_imp l (clauses.cons_clause l C) -->
or_intro_1 (lprop l) (cprop C) or_intro_1 (lprop l) (cprop C)
[l1,l2,C] magic_or_imp l1 (clauses.cons_clause l2 C) --> [l1,l2,C] magic_or_imp l1 (clauses.cons_clause l2 C) -->
H => or_intro_2 (lprop l2) (cprop C) (magic_or_imp l1 C H). H => or_intro_2 (lprop l2) (cprop C) (magic_or_imp l1 C H).
(; /!\ magic_remove l C H only reduces if l ∈ C ;) (; /!\ magic_remove l C H only reduces if l ∈ C ;)
def magic_remove (l : clauses.litteral) (C : clauses.clause) (H : cproof (clauses.cons_clause l C)) : cproof C := def magic_remove (l : clauses.literal) (C : clauses.clause) (H : cproof (clauses.cons_clause l C)) : cproof C :=
fol.or_elim (lprop l) (cprop C) (cprop C) H fol.or_elim (lprop l) (cprop C) (cprop C) H
(magic_or_imp l C) (HC => HC). (magic_or_imp l C) (HC => HC).
...@@ -333,7 +333,7 @@ def remove_nth_q : nat -> clauses.qclause -> clauses.qclause. ...@@ -333,7 +333,7 @@ def remove_nth_q : nat -> clauses.qclause -> clauses.qclause.
[n,A,p] remove_nth_q n (clauses.qc_all A p) --> [n,A,p] remove_nth_q n (clauses.qc_all A p) -->
clauses.qc_all A (x => remove_nth_q n (p x)). clauses.qc_all A (x => remove_nth_q n (p x)).
(; /!\ remove_nth_q_correct only reduces if the nth clauses.litteral in Q appears twice ;) (; /!\ remove_nth_q_correct only reduces if the nth clauses.literal in Q appears twice ;)
def remove_nth_q_correct : n : nat -> Q : clauses.qclause -> qcproof Q -> qcproof (remove_nth_q n Q). def remove_nth_q_correct : n : nat -> Q : clauses.qclause -> qcproof Q -> qcproof (remove_nth_q n Q).
[n,C,H] remove_nth_q_correct n (clauses.qc_base C) H --> [n,C,H] remove_nth_q_correct n (clauses.qc_base C) H -->
magic_remove (nth_lit n C) (remove_nth n C) (cycle_nth_correct n C H) magic_remove (nth_lit n C) (remove_nth n C) (cycle_nth_correct n C H)
...@@ -341,12 +341,12 @@ def remove_nth_q_correct : n : nat -> Q : clauses.qclause -> qcproof Q -> qcproo ...@@ -341,12 +341,12 @@ def remove_nth_q_correct : n : nat -> Q : clauses.qclause -> qcproof Q -> qcproo
fol.all_intro A (x => qcprop (remove_nth_q n (p x))) fol.all_intro A (x => qcprop (remove_nth_q n (p x)))
(x => remove_nth_q_correct n (p x) (fol.all_elim A (x => qcprop (p x)) H x)). (x => remove_nth_q_correct n (p x) (fol.all_elim A (x => qcprop (p x)) H x)).
(; only reduces if the ith and jth litterals are unifiable ;) (; only reduces if the ith and jth literals are unifiable ;)
def unify_litterals_q : nat -> nat -> Q : clauses.qclause -> qc_subst Q. def unify_literals_q : nat -> nat -> Q : clauses.qclause -> qc_subst Q.
[i,j,C] unify_litterals_q i j (clauses.qc_base C) --> [i,j,C] unify_literals_q i j (clauses.qc_base C) -->
unify_litterals (nth_lit i C) (nth_lit j C) unify_literals (nth_lit i C) (nth_lit j C)
[i,j,P] unify_litterals_q i j (clauses.qc_all _ P) --> [i,j,P] unify_literals_q i j (clauses.qc_all _ P) -->
x => unify_litterals_q i j (P x). x => unify_literals_q i j (P x).
(; remove useless quantifications, that is quantifications on unused variables ;) (; remove useless quantifications, that is quantifications on unused variables ;)
(; removes quantifers on unused variables ;) (; removes quantifers on unused variables ;)
...@@ -366,12 +366,12 @@ def unquantify_correct : Q : clauses.qclause -> qcproof Q -> qcproof (unquantify ...@@ -366,12 +366,12 @@ def unquantify_correct : Q : clauses.qclause -> qcproof Q -> qcproof (unquantify
(x => unquantify_correct (P x) (fol.all_elim A (x => qcprop (P x)) H x)). (x => unquantify_correct (P x) (fol.all_elim A (x => qcprop (P x)) H x)).
def factor (i : nat) (j : nat) (Q : clauses.qclause) : clauses.qclause := def factor (i : nat) (j : nat) (Q : clauses.qclause) : clauses.qclause :=
remove_nth_q j (qclause_specialize Q (lqc_subst Q (unify_litterals_q i j Q))). remove_nth_q j (qclause_specialize Q (lqc_subst Q (unify_literals_q i j Q))).
def factor_correct (i : nat) (j : nat) (Q : clauses.qclause) (H : qcproof Q) : qcproof (factor i j Q) := def factor_correct (i : nat) (j : nat) (Q : clauses.qclause) (H : qcproof Q) : qcproof (factor i j Q) :=
remove_nth_q_correct j remove_nth_q_correct j
(qclause_specialize Q (lqc_subst Q (unify_litterals_q i j Q))) (qclause_specialize Q (lqc_subst Q (unify_literals_q i j Q)))
(qclause_specialize_correct Q (lqc_subst Q (unify_litterals_q i j Q)) H). (qclause_specialize_correct Q (lqc_subst Q (unify_literals_q i j Q)) H).
(; Universally quantified pairs of clauses (of the form (; Universally quantified pairs of clauses (of the form
∀x₁…∀xₙ. C∧D). This is usefull as an intermediate shape for the ∀x₁…∀xₙ. C∧D). This is usefull as an intermediate shape for the
...@@ -443,7 +443,7 @@ def qclause_merge_correct : Q : clauses.qclause -> Q' : clauses.qclause -> qcpro ...@@ -443,7 +443,7 @@ def qclause_merge_correct : Q : clauses.qclause -> Q' : clauses.qclause -> qcpro
def biclause_unify : nat -> nat -> B : biclause -> bc_subst B. def biclause_unify : nat -> nat -> B : biclause -> bc_subst B.
[i,j,C,D] biclause_unify i j (bc_base (bclause_i C D)) --> [i,j,C,D] biclause_unify i j (bc_base (bclause_i C D)) -->
unify_opposite_litterals (nth_lit i C) (nth_lit j D) unify_opposite_literals (nth_lit i C) (nth_lit j D)
[i,j,A,P] biclause_unify i j (bc_all A P) --> [i,j,A,P] biclause_unify i j (bc_all A P) -->
x => biclause_unify i j (P x). x => biclause_unify i j (P x).
...@@ -634,7 +634,7 @@ def atom_of_prop_correct : p : prop -> proof p -> aproof (atom_of_prop p). ...@@ -634,7 +634,7 @@ def atom_of_prop_correct : p : prop -> proof p -> aproof (atom_of_prop p).
def atom_of_prop_complete : p : prop -> aproof (atom_of_prop p) -> proof p. def atom_of_prop_complete : p : prop -> aproof (atom_of_prop p) -> proof p.
[H] atom_of_prop_complete (fol.apply_pred _ _) H --> H. [H] atom_of_prop_complete (fol.apply_pred _ _) H --> H.
def lit_of_prop : prop -> clauses.litteral. def lit_of_prop : prop -> clauses.literal.
[p] lit_of_prop (fol.imp p fol.false) --> clauses.neg_lit (atom_of_prop p) [p] lit_of_prop (fol.imp p fol.false) --> clauses.neg_lit (atom_of_prop p)
[p] lit_of_prop p --> clauses.pos_lit (atom_of_prop p). [p] lit_of_prop p --> clauses.pos_lit (atom_of_prop p).
......
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