Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Ordered Resolution vs. Connection Graph resolution
| Book Series | Lecture Notes in Computer Science |
| Publisher | Springer Berlin / Heidelberg |
| ISSN | 0302-9743 (Print) 1611-3349 (Online) |
| Volume | Volume 2083/2001 |
| Book | Automated Reasoning |
| DOI | 10.1007/3-540-45744-5 |
| Copyright | 2001 |
| ISBN | 978-3-540-42254-9 |
| DOI | 10.1007/3-540-45744-5_14 |
| Pages | 182-194 |
| Subject Collection | Computer Science |
| SpringerLink Date | Monday, January 01, 2001 |
| |
|
Ordered Resolution vs. Connection Graph resolution
Reiner Hähnle4 , Neil V. Murray5 and Erik Rosenthal6 
| (4) |
Dept. of Computing Science, Chalmers University of Technology, S-41296, Gothenburg, Sweden |
| (5) |
Department of Computer Science, State University of New York, Albany, NY 12222, USA |
| (6) |
Department of Mathematics, University of New Haven, West Haven, CT 06516, USA |
Abstract
Connection graph resolution (cg-resolution) was introduced by Kowalski as a means of restricting the search space of resolution.
Several researchers expected unrestricted connection graph (cg) resolution to be strongly complete until Eisinger proved that
it was not. In this paper, ordered resolution is shown to be a special case of cg-resolution, and that relationship is used
to prove that ordered cg-resolution is strongly complete. On the other hand, ordered resolution provides little insight about
completeness of first order cg-resolution and little about the establishment of strong completeness from completeness. A first
order version of Eisinger’s cyclic example is presented, illustrating the difficulties with first order cg resolution. But
resolution with selection functions does yield a simple proof of strong cg-completeness for the unit-refutable class.
Acknowledgement Bernhard Beckert noticed an error in an earlier version and gave several useful and simplifying suggestions. A discussion
with Harald Ganzinger helped clarify several issues.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|