Solving simplifications ordering constraints

Johann, Patricia; Socher-Ambrosius, Rolf

Datensatz

DATENSATZ AKTIONENEXPORT

Zur Ablage hinzufügen

Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben

Bericht

Solving simplifications ordering constraints

MPG-Autoren

/persons/resource/persons44009

Socher-Ambrosius, Rolf
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen

Es sind keine externen Ressourcen hinterlegt

Volltexte (beschränkter Zugriff)

Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.

Volltexte (frei zugänglich)

MPI-I-93-256.pdf
(beliebiger Volltext), 119KB

Ergänzendes Material (frei zugänglich)

Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar

Zitation

Johann, P., & Socher-Ambrosius, R.(1993). Solving simplifications ordering constraints (MPI-I-93-256). Saarbrücken: Max-Planck-Institut für Informatik.

Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0014-B4A1-D

Zusammenfassung

This paper presents a decision procedure for the existential fragment of the theory of simplification oderings, which extends previous work by D. Plaisted. We consider both solvability in the given signature and solvability in an extended signature. The algorithm has cubic complexity for pure conjunctive ordering constraints in the extended signature case. However, we show that some slight extensions of the basic problem are NP-complete, for example, if the ordering is interpreted as a total simplification ordering or a lexicographic path ordering (LPO) with arbitrary precedence.