School of Computing

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)},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014