Finding Resolution K-Transformations

Smaus, Jan - Georg

Lokale TagsFreigabegeschichteDetailsÜbersicht

Finding Resolution K-Transformations

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

Item is Freigegeben

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:

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

Genre: Hochschulschrift

ausblenden:

Urheber:
Smaus, Jan - Georg¹, Autor

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

Inhalt

einblenden:

ausblenden:

Schlagwörter: -

Zusammenfassung: 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.