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.