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.
My Menu
Saved Items

Ordered Resolution vs. Connection Graph resolution

Reiner HähnleContact Information, Neil V. MurrayContact Information and Erik RosenthalContact Information

(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.

Contact Information Reiner Hähnle
Email: reiner@cs.chalmers.se

Contact Information Neil V. Murray
Email: nvm@cs.albany.edu

Contact Information Erik Rosenthal
Email: brodsky@charger.newhaven.edu
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.109 • Server: MPWEB25
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)