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 |

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. |

Keywords: | formula equation; fixed-point theorem; Hoare logic; inductive theorem proving |

URI: | https://doi.org/10.34726/hss.2021.85542 http://hdl.handle.net/20.500.12708/17585 |

DOI: | 10.34726/hss.2021.85542 |

Library ID: | AC16215810 |

Organisation: | E104 - Institut für Diskrete Mathematik und Geometrie |

Publication Type: | Thesis Hochschulschrift |

Appears in Collections: | Thesis |

#### Files in this item:

File | Description | Size | Format | |
---|---|---|---|---|

Kloibhofer Johannes - 2021 - A fixed-point theorem for Horn formula equations.pdf | 655.52 kB | Adobe PDF | View/Open |

#### Page view(s)

24
checked on Jun 21, 2021

#### Download(s)

10
checked on Jun 21, 2021

#### Google Scholar^{TM}

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