A | |
| Admissible |
making a context unifier admissible
|
B | |
| Bound |
iterative deepening bound
|
C | |
| ClauseApproxTable [Term] |
a specialized
Hashtbl with clauses as keys.
|
| ClauseTable [Term] |
a specialized
Hashtbl with clauses as keys.
|
| Config |
configuration for a derivation
|
| Const |
global constants
|
| Context |
context with operations
|
| Context_unifier |
basic types for and operations on context unifiers
|
| Context_unifier_check |
context unifier validity check
|
| Context_unifier_search |
search for context unifiers
|
| Context_unifier_space |
a problem clause
|
| Counter |
int counter
|
D | |
| Darwin |
proof procedure
|
| Discrimination_tree |
term indexing with a discrimination tree
|
E | |
| Equality |
equality by axiomatization
|
F | |
| Finite_domain |
finite domain model finding
|
| Flags |
command line evaluation
|
H | |
| Heap |
The classic imperative array based heap data structure.
|
| Heap |
heap structures
|
I | |
| IntTable [Tools] |
a specialized
Hashtbl with ints as keys.
|
J | |
| Jumping |
random jumps within the search space
|
L | |
| Lemma |
lemma learning
|
| Lemma_grounded |
grounded lemma generation
|
| Lemma_lifted |
lifted lemma learning
|
| Lemma_propositional |
propositional 'lemma' generation
|
| LiteralTable [Term] |
a specialized
Hashtbl with literals as keys.
|
| LiteralTypeTable [Term] |
a specialized
Hashtbl with literal types as keys,
that is not the concrete literal but it's sign and predicate symbol.
|
| Log |
derivation log
|
M | |
| MinMaxHeap [Heap] |
An imperative array based min-max heap data structure.
|
P | |
| PPreserving [Subst] |
recompute = false; p_preserving = true
|
| Preprocessing_equality |
simplifications based on equality
|
| Preprocessing_pure |
removes pure clauses
|
| Preprocessing_resolution |
computes short resolvents
|
| Preprocessing_split_ground |
splitting of variable disjoint clause parts
|
| Preprocessing_split_nonground |
splitting of clause parts
|
| Preprocessing_unit |
unit subsumption and resolution
|
| Preserving [Subst] |
recompute = false; p_preserving = false
|
common print functions and constants used in ouput
| |
| Problem |
a problem clause set
|
| Problem_literals |
checking of problem literals against new context literals
|
R | |
| RPPreserving [Subst] |
recompute = true; p_preserving = true
|
| RPreserving [Subst] |
recompute = true; p_preserving = false
|
| Read_darwin |
reads files in darwin's format
|
| Read_tme |
reads tme files
|
| Read_tptp |
reads tptp files
|
S | |
| SearchAll [Context_unifier_search] |
search for Assert, Close, and Split context unifiers.
|
| SearchAssert [Context_unifier_search] |
search for Assert context unifiers only.
|
| SearchClose [Context_unifier_search] |
search for Close context unifiers only.
|
| SearchCloseAssert [Context_unifier_search] |
search for Assert and Close context unifiers only.
|
| SearchSplit [Context_unifier_search] |
search for Split context unifiers only.
|
| Selection |
selection of a split or assert literal
|
| Selection_assert |
selection of assert candidates
|
| Selection_lookahead |
Close lookahead for candidates
|
| Selection_split |
selection of split candidates
|
| Selection_types |
common types for selection modules
|
| Sort_inference |
infers sorts based on a clause set
|
| Stack |
imperative stack
|
| State |
choice point (decision level) management
|
| State_backtrack |
backtracking of module
State
|
| Statistic |
derivation statistic
|
| StringTable [Tools] |
a specialized
Hashtbl with strings as keys.
|
| Subst |
a substitution
|
| Symbol |
constant and function symbols
|
| SymbolTable [Symbol] |
a specialized
Hashtbl with symbols as keys.
|
T | |
| Term |
terms, literals, clauses
|
| TermTable [Term] |
a specialized
Hashtbl with terms as keys.
|
| Term_attributes |
computation and comparison of term attributes
|
| Term_indexing |
term indexing
|
| Tools |
general functions
|
U | |
| Unification |
term unification
|
V | |
| Var |
universal and parameteric variables
|
| VarTable [Var] |
a specialized
Hashtbl with variables as keys.
|
| VarTable [Subst] |
a specialized
Hashtbl with variables as keys.
|
Z | |
| Zip_wrapper |
wrapper for reading zipped files
|