|
|
Theta-Subsumption
| Description: |
The θ-subsumtion is a correct, but incomplete inference operator for clauses with
the advantage of being feasible, while correct and complete inference operators in full first order
logic are known to be algorithmically intractable.
- A clause C1 θ-subsumes another clause C2, if and only if
a substitution θ exists, such that C1θ ⊆ C2.
- If C1 θ-subsumes C2 then C1 implies
C2.
Θ-subsumption may also be used for quasi-ordering the hypothesis language of clauses. |
|
|
