Finite Herbrand Models for Monadic Clauses with Unary Function Symbols

Theses

• Suggested Thesis Topics
• Completed Theses
  • Algebra und Diskrete Strukturen
  • Automatentheorie
  • Computational Logic
  • Knowledge-aware Artificial Intelligence
  • Logische Programmierung und Argumentation
  • Verifikation und formale quantitative Analyse
  • Wissensbasierte Systeme
• Currently Ongoing Theses

Toggle side column

Finite Herbrand Models for Monadic Clauses with Unary Function Symbols

Master's thesis by Muhammad Zahid Zia

•   Supervisor Franz Baader, Stefan Borgwardt
•   Automatentheorie
•   1 Oktober 2015 – 14 April 2016
•   Download

Decidability of First Order Logic (FOL) is a key and active research area in logic and computer science. As FOL is undecidable in its general form, a lot of research is focused on finding classes of FOL which are decidable and studying their properties. In this thesis, we work on one such decidable fragment that only allows monadic predicate and function symbols (with the exception of one constant). We also allow just one variable in the formulas.

Research in Logic generally does not concentrate on the finiteness of interpretations. Yet, for any realistic and practical knowledge representation purpose we only have finitely many resources to represent the real world. Therefore we focus on finding the finite Herbrand models for the above mentioned class. We also provide a terminating decision procedure for the existence of a finite Herbrand model for this restricted fragment of FOL. In the end we provide some optimizations and variants of the original algorithm for better performance on certain problems.