2 Prolog and First-Order Logic

We would like to use first order logic as a semantic representation formalism, and we want to deal with it in Prolog. So obviously the first thing we need is a way of representing in Prolog the basic entitities that play a role in first order logic. We've seen that these are first-order models, first-order formulae and vocabularies. The first part of this lecture discusses the Prolog representations we will choose for them.

Then, we turn to the notion of truth in a model. We approach this notion in Prolog by implementing a simple first-order model checker (or semantic evaluator). The model checker takes a first-order formula and an (exact) first-order model as input and checks whether the formula is true in the model.

Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)