Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Canonical sources for HOL4 theorem-proving system. Branch `develop` is where “mainline development” occurs; when `develop` passes our regression tests, `master` is merged forward to catch up.
A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.
This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.