Skip to content
/ trustee Public

[wip] A LCF-style kernel of trust intended for certified ATP and proof checking for FOL/HOL.

Notifications You must be signed in to change notification settings

c-cube/trustee

Repository files navigation

Trustee build

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/

About

[wip] A LCF-style kernel of trust intended for certified ATP and proof checking for FOL/HOL.

Topics

Resources

Stars

Watchers

Forks

Packages

No packages published

Languages