<div class="csl-bib-body">
<div class="csl-entry">Zivota, S. (2021). <i>On formula equations and invariant generation</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.86440</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2021.86440
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/17552
-
dc.description.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
dc.description.abstract
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.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Formelgleichungen
de
dc.subject
Beweistheorie
de
dc.subject
dynamische Logik
de
dc.subject
affine Geometrie
de
dc.subject
formula equations
en
dc.subject
proof theory
en
dc.subject
dynamic logic
en
dc.subject
affine geometry
en
dc.title
On formula equations and invariant generation
en
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2021.86440
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Sebastian Zivota
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
tuw.publication.orgunit
E104 - Institut für Diskrete Mathematik und Geometrie
-
dc.type.qualificationlevel
Doctoral
-
dc.identifier.libraryid
AC16212533
-
dc.description.numberOfPages
142
-
dc.thesistype
Dissertation
de
dc.thesistype
Dissertation
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.advisor.orcid
0000-0002-6461-5982
-
item.languageiso639-1
en
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_db06
-
item.fulltext
with Fulltext
-
item.openairetype
doctoral thesis
-
item.grantfulltext
open
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E104-02 - Forschungsbereich Computational Logic
-
crisitem.author.parentorg
E104 - Institut für Diskrete Mathematik und Geometrie