Finite Herbrand Models for Monadic Clauses with Unary Function Symbols

From International Center for Computational Logic
Toggle side column

Finite Herbrand Models for Monadic Clauses with Unary Function Symbols

Master's thesis by Muhammad Zahid Zia
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.