<div class="csl-bib-body">
<div class="csl-entry">Kloibhofer, J. (2021). <i>A fixed-point theorem for Horn formula equations</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.85542</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2021.85542
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/17585
-
dc.description
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
-
dc.description.abstract
Formula equations are logical equations in which the unknowns are formulas. They naturally occur in many areas like program verification or automated theorem proving. In these communities similar problems are treated independently. Our motivation is to state general theorems about formula equations which then will be used to generalize and simplify results in various different applications. In this thesis we treat the special case of Horn formula equations, this restriction is justified as it covers many applications. For Horn formula equations we are able to compute canonical solutions if a solution exists. This will be achieved by defining an operator such that every solution of the Horn formula equation is a fixed point of it. Now the least fixed point, which exists due to the Knaster-Tarski theorem, turns out to always be a solution if there exists one. This canonical solution will be described by least fixed-point formulas. Furthermore the canonical solution implies every solution of the Horn formula equation. We then use the Horn fixed-point theorem to obtain a first-order approximation of second-order formulas as well as to get a different perspective on Hoare triples in program verification and to get more insights in inductive theorem proving.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
formula equation
en
dc.subject
fixed-point theorem
en
dc.subject
Hoare logic
en
dc.subject
inductive theorem proving
en
dc.title
A fixed-point theorem for Horn formula equations
en
dc.title.alternative
Ein Fixpunktsatz für Horn-Formelgleichungen
de
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.85542
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Johannes Kloibhofer
-
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
Diploma
-
dc.identifier.libraryid
AC16215810
-
dc.description.numberOfPages
47
-
dc.thesistype
Diplomarbeit
de
dc.thesistype
Diploma Thesis
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.advisor.orcid
0000-0002-6461-5982
-
item.openaccessfulltext
Open Access
-
item.openairecristype
http://purl.org/coar/resource_type/c_bdcc
-
item.grantfulltext
open
-
item.mimetype
application/pdf
-
item.languageiso639-1
en
-
item.openairetype
master thesis
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E104-02 - Forschungsbereich Computational Logic
-
crisitem.author.parentorg
E104 - Institut für Diskrete Mathematik und Geometrie