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.

• 2.1 A Simple Model Checker
  • 2.1.1 Representing Vocabularies
  • 2.1.2 Representing Simple Formulae
  • 2.1.3 Representing Complex Formulae
  • 2.1.4 Representing Models
  • 2.1.5 Another Example
  • 2.1.6 Semantic Evaluation
  • 2.1.7 Evaluating Complex Formulae
  • 2.1.8 Quantifiers
  • 2.1.9 Checking Models

• 2.2 Refinements
  • 2.2.1 Problem One: Unknown Vocabulary
  • 2.2.2 Problem Two: Formulae with Free Variables
  • 2.2.3 Refining the Implementation

• 2.3 File Listing
  • 2.3.1 All modules for the model checker

• 2.4 Exercises