| Admissible |
making a context unifier admissible
|
| Bound |
iterative deepening bound
|
| 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
|
| Darwin |
proof procedure
|
| Discrimination_tree |
term indexing with a discrimination tree
|
| Equality |
equality by axiomatization
|
| Finite_domain |
finite domain model finding
|
| Flags |
command line evaluation
|
| Heap |
heap structures
|
| Jumping |
random jumps within the search space
|
| Lemma |
lemma learning
|
| Lemma_grounded |
grounded lemma generation
|
| Lemma_lifted |
lifted lemma learning
|
| Lemma_propositional |
propositional 'lemma' generation
|
| Log |
derivation log
|
| 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
|
common print functions and constants used in ouput
| |
| Problem |
a problem clause set
|
| Problem_literals |
checking of problem literals against new context literals
|
| Read_darwin |
reads files in darwin's format
|
| Read_tme |
reads tme files
|
| Read_tptp |
reads tptp files
|
| 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
|
| Subst |
a substitution
|
| Symbol |
constant and function symbols
|
| Term |
terms, literals, clauses
|
| Term_attributes |
computation and comparison of term attributes
|
| Term_indexing |
term indexing
|
| Tools |
general functions
|
| Unification |
term unification
|
| Var |
universal and parameteric variables
|
| Zip_wrapper |
wrapper for reading zipped files
|