This site contains the documentation for the Calculemus library.
The library provides lexer, parsing and printing for propositional and first order logic together with a wide range of theorem proving techniques both automated and with interaction human-machine.
It is built on the F# porting of the OCaml code from John Harrison's book Handbook of Practical Logic and Automated Reasoning made by Jack Pappas, Eric Taucher, Anh-Dung Phan.
Compared to the original code (and also to the following F# porting) changes or new functions are introduced with the main intention being to provide greater details in certain aspects. However, the differences with the code described in the book are so minimal that the correspondence should always be clear.
The following namespaces are available:
Calculemus - The main namespace with the specific thematics.
Calculemus.Lib - The library with basic functions for general implementation.