I | |
| Id [Ast_tptp] | |
| Id [Tptp] | |
| Id [Ast_zf] | |
| Id [Zf] | |
| Id [Ast_smtlib] | |
| Id [Smtlib] | |
L | |
| Logic [Stmt_intf] | |
| Logic [Term_intf] | |
| Logic [Id_intf] | |
S | |
| S [Logic.Make] |
The type of language modules.
|
| S [Language_intf] | |
| S [Location_intf] | |
| S [Parse_intf] | |
| S [Lex_intf] | |
| S [ParseLocation] |
An anstract module type for providing locations.
|
| Statement [Ast_tptp] | |
| Statement [Tptp] |
Implementation requirement for the TPTP format.
|
| Statement [Ast_zf] | |
| Statement [Zf] |
Implementation requirements for the Zipperposition format.
|
| Statement [Ast_smtlib] | |
| Statement [Smtlib] |
Implementation requirement for the Smtlib format.
|
| Statement [Ast_dimacs] | |
| Statement [Dimacs] |
Implementation requirement for the Dimacs format.
|
T | |
| Term [Ast_tptp] | |
| Term [Tptp] | |
| Term [Ast_zf] | |
| Term [Zf] | |
| Term [Ast_smtlib] | |
| Term [Smtlib] | |
| Term [Ast_dimacs] | |
| Term [Dimacs] |