Information

Prove Empty Clause Data : a list of clauses in the panel Clauses
  • If the list is syntactically wrong, the system prints an red error message .
  • If the prover can deduce the empty clause, its proof is displayed.

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

and, you can impose limits in the proof search The trace button allows to follow the progress of the proof algorithm.

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.

  1. The list Δ(0) is obtained by reducing the list of clauses of the panel Clauses and the list Θ(0) is empty.
  2. The list Δ(i+1) is obtained as follows
    1. We build the set of resolvants between the clauses of Δ(i) and the clauses of Δ(i) or Θ(i) and we reduced this set of resolvants
    2. We remove from this set, the clauses subsumed by a clause of Δ(i) or Θ(i)
  3. The list Θ(i+1) is obtained by removing from the clauses of Δ(i) and Θ(i) the clauses subsumed by a clause of Δ(i+1)

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