The theoretical basis of this Model Elimination prover is described here in
english and
in french.
A chain is list of A-literal and B-literal. A B-literal is a literal in the usual sense.
A A-literal, also called literal ancestor, is a literal beetween brackets followed by an integer,
the scope of the litteral.
Here is an example of a chain : p(x) [q(x,y)]0 r(z) [-q(a,b)]1.
The scope of the first ancestor literal is 0 and the scope of
the second ancestor literal is 1.
Let Γ be a list of clauses. A derivation from Γ is a list of chains
Ci (i from 1 to n) such that
C1 is element of Γ and Ci+1 (i from 1 to n-1) is obtained from
Ci by one of the rules,
extension with a element of Γ, reduction and removal.
- Extension from Γ:
Let LU be a chain beginning with the B-literal L. Let VMW a copy of an element of Γ
where M is a literal and whose
variables do not appear in LU. Let us suppose that there exists a most general unifier σ
unifying L and the opposite
of M. The chain σ(VW[L]0U) is obtained by extension of LU from Γ.
The initial scope of the new literal ancestor is 0.
- Reduction :
Let LU[M]V a chain, where L is a literal and [M] an ancestor literal.
Let us suppose that there exists a most general
unifier σ unifying L and the opposite of M.
The chain σ(U[M]V) is obtained by reduction of LU[M]V.
The scope of [M] becomes the maximum of its scope before the
reduction and the number of literal ancestors of U.
- Removal :
Let [L]U be a chain benginning with the literal ancestor [L].
The chain U is obtained by removal on [L]U.
Let D the disjunction of the opposite of all the literal ancestors of LU,
whose scope is equal to the number of
lteral ancestors to their left.
This disjunction is a lemma deduced from Γ. The scope from these literal ancestors
is decremented.
With the button Max time of proof, you can limit in seconds the time allocated to the prover.
With the button
Max length of proof, you can limit the length of the derivations explored by the prover.
Let n be the maximum length set for the derivations.
With the button Prove Empty Clause without Lemma, the prover explored once all the derivations of
length at most n and
stops when it discovers a derivation of the empty clause or when there is no derivation of the empty clause.
With the button Prove Empty Clause with Lemma, the prover explored all the derivations of
length at most n and
stops when it discovers a derivation of the empty clause.
During this first research of a derivation of empty clause, the prover
collect all the lemmas not subsumed by the given clauses.
When this research is finished without discovering a derivation
of empty clause, the prover starts a second research of such a derivation,
from the given clauses and from the lemmas added during the first research.
The prover is complete, that means, if the list of clauses is unsatisfiable and
if there is no limit of time and length of
derivation, it will find a derivation of the empty clause.