Skip to main content
Kent Academic Repository

Resolution K-Transformations

Smaus, Jan-Georg (1996) Resolution K-Transformations. Other masters thesis, Universitaet des Saarlandes (Max-Planck-Institut fuer Informatik). (KAR id:21395)

Language: English
Download this file
[thumbnail of KSmaus.pdf]
Language: English
Download this file
[thumbnail of]


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.

Item Type: Thesis (Other masters)
Uncontrolled keywords: automated theorem proving, clause sets, transitivity, Euclideanness
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 06 Sep 2009 22:47 UTC
Last Modified: 16 Nov 2021 09:59 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.