Flattening, generalizations of clauses and absorption algorithms
January 1991
Research Paper
| Related Files |
|---|
View PDF Version
(eur-few-cs-91-02.pdf, 0.1MB) |
In predicate logic, flattening can be used to replace terms with functions by variables. It can also be used for expressing absorption in inverse resolution. This has been done by Rouveirol and Puget. In this article three kinds of absorption algorithms are compared.
Keywords
Automatically Extracted Terms
- clause
- substitution
- generalization
- variable
- literal
- algorithm
- term partitions
- example
- partition
- resolution
- problem
- subclause
- block
- clause c
- tree substitutions
- occurrence
- condition
- argument
- term occurrences
- stage
