Title: On formula equations and invariant generation
Language: English
Authors: Zivota, Sebastian 
Qualification level: Doctoral
Advisor: Hetzl, Stefan 
Issue Date: 2021
Number of Pages: 142
Qualification level: Doctoral
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.

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.
Keywords: Formelgleichungen; Beweistheorie; dynamische Logik; affine Geometrie
formula equations; proof theory; dynamic logic; affine geometry
URI: https://doi.org/10.34726/hss.2021.86440
http://hdl.handle.net/20.500.12708/17552
DOI: 10.34726/hss.2021.86440
Library ID: AC16212533
Organisation: E100 - Fakultät für Mathematik und Geoinformation 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

7
checked on Jun 10, 2021

Download(s)

13
checked on Jun 10, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.