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.