Information |
Prove Empty Clause | Data: two lists of clauses, a not empty list called the support list
and a list called the usable list.
|
The prover is complete, that means, if the usable list is satisfiable and if the concatenation of support and usable lists is unsatisfiable and if there is no limit of time and size, it will deduce the empty clause. You can impose two limits in the proof search
You can find the theoretical basis for this prover in the book
logique et démonstration automatique, and in the course of logic
inf402 given at
the university grenoble-alpes.
We describe below the strategy followed by our prover, that is an adaptation to the first order logic of
the prover9 variant of the complete strategy
(La variante prover9 de la stratégie complète) described in the book above.
Remark : prover9 is an excellent prover, more complete and much
more efficient that my prover, written by Mccune, who died in 2011.
A clause C subsumes a clause D if there a substitution σ such that all the litterals of σ(C) are
litterals of D. Reducing a list of clauses means removing from this list the valid clauses (the clauses containing
two opposed litterals) and the clauses subsumed by another clause of the list. Therefore the list of clauses
p(a) q(f(x)), q(b) -q(b) r(c), p(x) is reduced in p(x). The prover builds for each integer i, from 0, two lists of clauses s(i) and u(i) and stops at the first integer k such that s(k) is the empty list. If u(k) contains the empty clause, the prover displays the proof of that clause.
|
examples | syntax | info | home | download | Last Modified : 18-Dec-2019 |