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

An Open Research Problem: Strong Completeness of R. Kowalski’s Connection Graph Proof Procedure

Jörg SiekmannContact Information and Graham WrightsonContact Information

(3)  Universität des Saarlandes, Stuhlsatzenhausweg, D-66123 Saarbrücken, Germany
(4)  Department of Computer Science and Software Engineering, The University of Newcastle, NSW, 2308, Australia
Abstract
The connection graph proof procedure (or clause graph resolution as it is more commonly called today) is a theorem proving technique due to Robert Kowalski. It is a negative test calculus (a refutation procedure) based on resolution. Due to an intricate deletion mechanism that generalises the well-known purity principle, it substantially refines the usual notions of resolution-based systems and leads to a largely reduced search space. The dynamic nature of the clause graph upon which this refutation procedure is based, poses novel meta-logical problems previously unencountered in logical deduction systems. Ever since its invention in 1975 the soundness, confluence and (strong) completeness of the procedure have been in doubt in spite of many partial results. This paper provides an introduction to the problem as well as an overview of the main results that have been obtained in the last twenty-five years.

Contact Information Jörg Siekmann
Email: siekmann@dfki.de

Contact Information Graham Wrightson
Email: graham@cs.newcastle.edu.au
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.106 • Server: mpweb20
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)