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



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.