A constructive proof assistant for second order logic.
CORE is a minimal proof assistant capable of verifying proofs in various axiomatic systems. See the proofs folder for an implementation of set theory.
To build, use make. The flag USE_CUSTOM_ALLOC determines whether the verifyier wraps the allocator, which is useful for debugging.
To install, copy the executable core created after building to /usr/bin.
CORE comes with a model of the Zermelo Fraenkel set theory axioms and appropriate proofs to show that definitions are well defined. To verify these files, simply
run core proofs/main.core. These example programs are an excellent way to get to know the language.
See the (incomplete) documentation for a detailed description of the language.
- Straight-forward syntax
- Detailed error messages
- Axiom schema
- Proof schema
- Built-in rules to seamlessly determine whether one sentence trivially implies another (See trivialtruth in the documentation for more information.)
- Import and include system for organizing results and applying proofs in multiple contexts