Generalization of Clauses Relative to a Theory |
| |
Authors: | Idestam-Almquist Peter |
| |
Affiliation: | (1) Department of Computer and Systems Sciences, Stockholm University, Electrum 230, S-164 40 Kista, Sweden |
| |
Abstract: | Plotkin's notions of relative -subsumption and relative least general generalization of clauses are defined for full clauses, and they are defined in terms of a kind of resolution derivations called C-derivations. Techniques for generalization of clauses relative to a theory, based on the V-operators or saturation in its original form, have primarily been developed for Horn clauses. We show that these techniques are incomplete for full clauses, which is due to the restricted form of resolution derivations considered. We describe a technique for generalization of clauses relative to a theory, which is based on a generalization of the original saturation technique. We prove that our technique properly inverts C-derivations, and that it is complete for full clauses w.r.t. relative -subsumption. |
| |
Keywords: | relative generalization RLGG full clauses |
本文献已被 SpringerLink 等数据库收录! |
|