A LCF-style kernel of trust intended for certified ATP and proof checking for FOL/HOL.
Brief list of features, current or being developed:
- core API with representation of terms and theorems, in
src/core/kernel.ml. Terms use De Bruijn indices for bound variables, are hashconsed, and polymorphism is semi-explicit (i.e. polymorphic constants are applied to types explicitly, but type quantifiers are still implicit). - an OpenTheory library with a parser and a verifier based on trustee,
in
src/opentheory/