A | |
| Arg [Dedukti] | |
| Arg [Coq] | |
| 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 [Coq] | Interface for exporting proofs. |
| 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 |
| S [Solver_types_intf] | |
| S [Res_intf] | |
| S [Expr_intf] | |
| S [Plugin_intf] | |
| S [Theory_intf] | |
| S [Formula_intf] |