No label defined (Q4400799)

This chapter is intended to provide the basic definitions of those logics which are used in several of the subsequent chapters of this volume. We have divided it into three main parts. First, we briefly introduce the syntax of first-order logic and define the standard (Tarskian) semantics for first-order logic. In addition, we sketch proof theory for first-order logic by presenting a Hilbert style and a natural deduction proof system. Then we turn to the basics of modal logics. The usual approach to give semantics to modal logics is by Kripke-structures. We briefly consider the axiomatization of several standard modal logics. We complete the section on modal logics by considering two special variants of modal logics for describing temporal evolution of systems: linear temporal logic and branching time logic. The third part of this logic primer deals with the formal foundations of logic programming and deductive databases. We define the notions of Herbrand model, fixpoint semantics, and SLD-resolution. Due to the fact that negation in logical rules causes a lot of problems we also consider different ways of defining semantics for logical programs with negation, in particular, we consider stratification, stable semantics, and well-founded semantics. For the entire collection see [Zbl 0889.00013].