Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-42866
Titel: | A Decision Procedure for Presburger Arithmetic with Functions and Equality |
VerfasserIn: | Krämer, F.-J. |
Sprache: | Englisch |
Erscheinungsjahr: | 1989 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | Many of the formulas one tends to encounter in program verification are contained in the quantifier-free Presburger Arithmetic and its extension by predicate and function symbols. Remarkable work for both the unextended and the extended class has been done by Robert Shostak. Particularly for the quantifier-free Presburger Arithmetic, he developed a very elegant algorithm based on the computation of loop residues in a graph. The algorithm decides the satisfiability of of a conjunction of atomic formulas of this theory. This diploma thesis presents the development of a decision procedure for the satisfiability of a conjunction of atomic formulas of the quantifier-free Presburger Arithmetic extended by predicate and function symbols: The EQUALITY_LOOP_RESIDUE procedure. This procedure combines both the concept of the LOOP_RESIDUE method in a refined version adjusted to the specific problems of the extended class and the concept of rewriting. The connection of this decision problem to ground terms is pointed out and a polynomial time algorithm for computing a canonical rewriting system equivalent to a finite set of ground equations recently (1988) presented by Gallier, Narendran, Plaisted, Raatz, and Snyder can be used as subprocedure in the newly developed decision procedure. The EQUALITY_LOOP_RESIDUE procedure does not only improve the decision process of the satisfiability of a conjunction of atomic formulas, but also the determination of the validity of a quantifier-free Presburger formula including predicate and function symbols. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-428667 hdl:20.500.11880/38566 http://dx.doi.org/10.22028/D291-42866 |
Schriftenreihe: | SEKI working paper : SWP ; SEKI-Projekt / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1860-5931] |
Band: | 89,4 |
Datum des Eintrags: | 30-Sep-2024 |
Fakultät: | SE - Sonstige Einrichtungen |
Fachrichtung: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
Professur: | SE - Sonstige |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
SEKI-Working-Paper-SWP-89-04_Krämer_A-Decision-Procedure-for-Presburger-Arithmetic-with-Functions-and-Equality.pdf | 62,5 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.