Information |
Prove Empty Clause | Data : a list of clauses in the panel Clauses
|
The prover is complete, that means, if the list of clauses is unsatisfiable and if there is no limit of time and size, it will deduce the empty clause. But you can choose, without preventing completeness, the type of resolution
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 complete strategy (stratégie complète ) described in the book above.
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 Δ(i) and Θ(i) and stops at the first integer k such that Δ(k) is the empty list. If Θ(k) contains the empty clause, the prover displays the proof of that clause.
|
examples | syntax | info | home | download | Last Modified : 02-Dec-2019 |