Modules

Here is a list of all modules:

Defining sorts of first-order logic
Defining function and predicate symbols of first-order logic
Defining terms and formulas of first-order logic
Defining proof certificates of unsatisfiability
SMT-LIB2 commands and proof checker, imperative style
SMT-LIB2 commands and proof checker, functional style