Finding Resolution K-Transformations

Smaus, Jan - Georg

Local TagsRelease HistoryDetailsSummary

Finding Resolution K-Transformations

Smaus, J.-.-G. (1996). Finding Resolution K-Transformations. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-ABDA-1 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-AD40-8

Genre: Thesis

Files

show Files

Locators

show

Creators

show

hide

Creators:
Smaus, Jan - Georg¹, Author

Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Content

show

hide

Free keywords: -

Abstract: Resolution K-transformations are faithful transformations between clause sets. The aim is to remove clauses like symmetry or transitivity from a clause set in order to eliminate or reduce recursivity and circularity in this clause set. It is shown that for any set of such clauses, a resolution K-transformation is likely to exist and can be found automatically. Clause K-transformations may be applied to reduce the search space of theorem provers, to eliminate loops in logic programs, to parallelise closure computation algorithms and to support automated complexity analysis.

Details

show

hide

Language(s): eng - English

Dates: Modified: 2010-03-12Accepted: 1996Date issued: 1996

Publication Status: Issued

Pages: -

Publishing info: Saarbrücken : Universität des Saarlandes

Table of Contents: -

Rev. Type: -

Identifiers: eDoc: 519486
Other: Local-ID: C1256104005ECAFC-2AADE6F45268922E412563EC007E34F6-Smaus96

Degree: Master

Event

show

Legal Case

show

Project information

show

Source

show