Skip to main content

Resolution K-Transformations

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


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: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 06 Sep 2009 22:47 UTC
Last Modified: 28 May 2019 14:00 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year