Commit 27989ea2 authored by Raphael CAUDERLIER's avatar Raphael CAUDERLIER

[doc] fix small mistakes in the documentation of the resolution module

parent 66b9cc9f
......@@ -773,11 +773,13 @@ combinator) and then uses the classical lemma
variables which are to be interpreted as universally quantified. A
*quantified clause* is an explicitly universally quantified clause.
The simplest way to define a clause is by parsing the corresponding
The types for atoms, litterals, clauses, and quantified clauses are
declared with their constructors in [[./fol/clauses.dk][fol/clauses.dk]]. However, the
simplest way to define a clause is by parsing the corresponding
proposition using the partial function
=resolution.qclause_of_prop=:
- =resolution.qclause_of_prop : fol.prop -> resolution.qclause=
- =resolution.qclause_of_prop : fol.prop -> clauses.qclause=
- =resolution.qclause_of_prop_correct : p : fol.prop -> fol.proof p -> resolution.qcproof (resolution.qclause_of_prop p)=
A resolution proof is a derivation of the empty clause
......@@ -786,11 +788,11 @@ combinator) and then uses the classical lemma
#+BEGIN_example
l₁ ∨ … ∨ lₙ σ = mgu(lᵢ, lⱼ)
-—————————————————————————————– Factorisation
———————————————————————————————— Factorisation
(l₁ ∨ … ∨ lⱼ₋₁ ∨ lⱼ₊₁ ∨ … ∨ lₙ)σ
l₁ ∨ … ∨ lₙ l'₁ ∨ … ∨ l'ₘ σ = mgu(lᵢ, ¬l'ⱼ)
——————————————————–—————————————————–————————–—––——————————————————— Resolution
——————————————————————————————————————————————————————————————————————— Resolution
(l₁ ∨ … ∨ lᵢ₋₁ ∨ lᵢ₊₁ ∨ … ∨ lₙ ∨ l'₁ ∨ … ∨ l'ⱼ₋₁ ∨ l'ⱼ₊₁ ∨ … ∨ l'ₘ)σ
#+END_example
......
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