2.1 A Simple Model Checker

In this part of the lecture, we'll write a first version of our model checker. This will turn out to be quite easy, but the implementation will still have various shortcomings. (In the second part of the lecture, we will fix the more obvious ones.) How should we implement a model checker? We have four principal tasks:

• Deciding how to represent (first-order) vocabularies.

• Deciding how to represent (first-order) formulas.

• Deciding how to represent (first-order) models.

• Specifying how (representations of) formulas are to be evaluated in (representations of) models.

So, let's start.

• 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