Wiki Agenda Contact Version française

A Certified First-Order Theorem Prover

This prover implements a tableaux method to find a proof of inconsistency for a set of first-order formulas given as input. The prover is proven correct (if it answers unsat then the input set is inconsistent) but not proven complete. This example appears as a case study in paper Verified Programs with Binders.

Authors: Martin Clochard

Topics: Semantics of languages

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

This example is split into several files.

download ZIP archive