Zivota, S. (2021). On formula equations and invariant generation [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.86440
formula equations; proof theory; dynamic logic; affine geometry
en
Abstract:
Diese Arbeit präsentiert Formelgleichungen—Formeln erster Stufe mit Prädikatenvariablen—als einen allgemeinen Formalismus zur Behandlung verschiedener Fragen in der Logik und der Informatik wie zum Beispiel das Auflösungsproblem oder Schleifeninvariantenerzeugung. Wir untersuchen das Verhältnis zwischen Schleifeninvarianten und induktivem Beweisen. Weiters erhalten wir Entscheidbarkeits- und Unentscheidbarkeitsresultate für Formelgleichungen mit verschiedenen Einschränkungen und über verschiedenen Theorien, insbesondere zeigen wir die Entscheidbarkeit des affinen Lösungsproblems.
de
We present formula equations—first-order formulas with unknowns standing for predicates—as a general formalism for treating certain questions in logic and computer science, like the Auflösungsproblem and loop invariant generation. We investigate the relationship between problems of loop invariant generation and inductive theorem proving. Furthermore, we obtain decidability and undecidability results for formula equations in certain languages, most notably that of affine terms over the rational numbers.