Information

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.

 examples | syntax | info | home | download Last Modified : 02-Dec-2019