Title: A fixed-point theorem for Horn formula equations
Other Titles: Ein Fixpunktsatz für Horn-Formelgleichungen
Language: English
Authors: Kloibhofer, Johannes 
Qualification level: Diploma
Advisor: Hetzl, Stefan 
Issue Date: 2021
Number of Pages: 49
Qualification level: Diploma
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.
Keywords: formula equation; fixed-point theorem; Hoare logic; inductive theorem proving
URI: https://doi.org/10.34726/hss.2021.85542
DOI: 10.34726/hss.2021.85542
Library ID: AC16215810
Organisation: E104 - Institut für Diskrete Mathematik und Geometrie 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

checked on Jun 21, 2021


checked on Jun 21, 2021

Google ScholarTM


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