OCML
The Operational Conceptual Modelling Language (OCML) combines logical reasoning in a frame-based language with the flexibility of extra-logical facilities like procedural attachment. It is implemented in Common Lisp, and has been tested with Lispworks, SBCL, and Allegro implementations. It is used by the Internet Reasoning System.

Repository: https://github.com/kmi/ocml

License: BSD-like

Theorem Provers