Wiki Agenda Contact English version

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.

Auteurs: Martin Clochard

Catégories: Semantics of languages

Outils: Why3

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

This example is split into several files.

download ZIP archive