Expand description
Resolution engine: proof search, unification, and term building. Resolution engine.
Implements second-order SLD resolution with backtracking.
Proof drives the search,
unification handles term matching, and
build constructs new terms from substitutions.
Modulesยง
- build
- Term building: construct new heap terms from clause templates and substitutions.
- proof
- Proof search via SLD resolution with backtracking and predicate invention.
- unification
- Unification algorithm and substitution management.