Kloibhofer, J. (2021). A fixedpoint theorem for Horn formula equations [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.85542
E104  Institut für Diskrete Mathematik und Geometrie

Date (published):
2021

Number of Pages:
47

Keywords:
formula equation; fixedpoint theorem; Hoare logic; inductive theorem proving
en
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 KnasterTarski theorem, turns out to always be a solution if there exists one. This canonical solution will be described by least fixedpoint formulas. Furthermore the canonical solution implies every solution of the Horn formula equation. We then use the Horn fixedpoint theorem to obtain a firstorder approximation of secondorder 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
Additional information:
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers