On the termination of clause graph resolution |
| |
Authors: | C. A. Johnson |
| |
Affiliation: | (1) Computer Science Department, University of Keele, ST5 5BG, Staffordshire, United Kingdom |
| |
Abstract: | This paper introducesextended clause graph resolution, a variant of Kowalski's clause graph resolution that is terminating at the full first-order level. This terminating variant is obtained by extending the definitions of clause graph and clause graph resolution to include more information about the interdependencies between links and clauses in the graph, by restricting purity slightly and by employing an exhaustive search of eligible links. |
| |
Keywords: | clause graphs resolution purity termination |
本文献已被 SpringerLink 等数据库收录! |
|