Next: About this document ...
Note on Paramodulation
Here's a better description of the paramodulation rule we talked about
in class. Let
- , , and be terms
- be a (possibly negated) literal that contains term as
a subexpression
-
, and
- and be (possibly empty) sets of literals.
Then, given a clause
and another clause
you may conclude
Here's an example. Given
and
we can conclude
by setting , , ,
, and
.
Michael G. Ross
2001-03-09