© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Resolution K-Transformations
Jan-Georg Smaus
Master's thesis, Universitaet des Saarlandes (Max-Planck-Institut fuer Informatik), Saarbruecken, Germany, February 1996.Abstract
Clause-K-transformations are faithful transformations between clause sets. When inferences are drawn on a clause set using resolution as inference rule, some clauses may be involved in particularly many resolution steps. Typically such a clause would express a very general property like the symmetry or transitivity of a relation. Most of these resolution steps do not contribute to inferring the empty clause.
Clause-K-transformations can be used to eliminate unnecessary resolution steps. A clause set is transformed by replacing a clause that is involved in particularly many resolution steps by {\em instances} of this clause. The more specific these instances are, the more this transformation will reduce the number of possible resolution steps. The criteria for the faithfulness of such a transformation can be tested automatically.
For clauses not containing function symbols, I have described a way to enumerate candidates for clause-K-transformations. With this I have found transformations for many clauses automatically.
I have also investigated eliminations for clauses containing function symbols (e.g.~condensed detachment) and eliminations of several clauses at the same time.
Download publication 690 kbytes (PostScript)
Bibtex Record
@mastersthesis{647, author = {Jan-Georg Smaus}, title = {Resolution {K}-{T}ransformations}, month = {February}, year = {1996}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {}, doi = {}, url = {http://www.cs.kent.ac.uk/pubs/1996/647}, address = {Saarbruecken, Germany}, school = {Universitaet des Saarlandes (Max-Planck-Institut fuer Informatik)}, }