The Deskolemization Page

The intention of this page is to provide examples of the elimination of Skolem functions from resolution proofs.

Complete Examples

Currently, I have only two complete examples worked out:

An example in PVS. The Bliksem output upon which it is based. ( [] means universal quantification, < > means existential quantification) The input to PVS. The proofs in PVS.
An example in Coq. It is constructed by hand, (and not based on a run of a theorem prover)

Examples of Individual Proof Steps.

I have checked lots of paramodulation steps with Bliksem. The Bliksem syntax is pretty straightforward. [ x , y ] means universal quantification. < x, y > means existential quantification.

paramodulation .
Paramodulate 0 = 1 into p( f(0,0), f(0,0), 0 ).
Paramodulate f(t(0)) = f(0) into p( f(t(0)), f(f(t(0))) on the assumption that f is a Skolem function.

A complete CNF-transformation.

I verified a complete CNF-transformation with Bliksem.