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
|