Information

Prove Empty Clause Data: two lists of clauses, a not empty list called the support list and a list called the usable list.
  • If the lists are syntactically wrong, the system displays an error message in red.
  • If the prover can deduce the empty clause from these two lists, its proof is displayed.

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

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 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.

  1. The list s(0) is obtained by reducing the support list and the list u(0) is obtained by reducing the usable list.
  2. The list s(i+1) is obtained as follows
    1. We choose a clause C belonging to s(i). You can use the button chosen clause to choose the first clause of this list with the smallest size, length or height.
    2. We computes the list P of all the resolvants beetwen C and the u(i) clauses.
    3. We computes the list Q of all the clauses of P not subsumed by a clause of s(i) or u(i).
    4. We computes the list R obtained by removing from s(i) the chosen clause C and the clauses subsumed by a clause of Q. The list s(i+1) is obtained by concatenating the lists R and Q.
  3. The list u(i+1) is obtained as follows. If the chosen clause C is subsumed by a clause of u(i), the list T is u(i) else the list T is obtained by adding C to u(i). The list u(i+1) is produced by removing from T the clauses subsumed by a clause of Q

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