A | |
| Arg [Dedukti] | |
| Arg [Dot] | |
| Arg [Tseitin] |
The implementation of formulas required to implement Tseitin's CNF conversion.
|
| Arg [Tseitin_intf] | |
S | |
| S [Backend_intf] | |
| S [Dedukti] | |
| S [Dot] |
Interface for exporting proofs.
|
| S [Tseitin] |
The exposed interface of Tseitin's CNF conversion.
|
| S [Mcsolver] |
The interface exposed by the solver.
|
| S [Solver] |
The interface of instantiated solvers.
|
| S [Solver_types] |
Interface for the internal types.
|
| S [External] |
Safe external interface of solvers.
|
| S [Res] |
Interface for a module manipulating resolution proofs.
|
| S [Tseitin_intf] | |
| S [Solver_intf] |
The external interface implemented by safe solvers, such as the one
created by the
Solver.Make and Mcsolver.Make functors.
|
| S [Solver_types_intf] | |
| S [Res_intf] | |
| S [Expr_intf] | |
| S [Plugin_intf] | |
| S [Theory_intf] | |
| S [Formula_intf] |