Introduction to Logic
Tools
for
Thought
 

Lesson 9 - Model Checking


9.1 Introduction

In Relational Logic, it is possible to analyze the properties of sentences in much the same way as in Propositional Logic. Given a sentence, we can determine its validity, satisfiability, and so forth by looking at possible truth assignments. And we can confirm logical entailment or logical equivalence of sentences by comparing the truth assignments that satisfy them and those that don't.

The main problem in doing this sort of analysis for Relational Logic is that the number of possibilities is even larger than in Propositional Logic. For a language with n object constants and m relation constants of arity k, the Herbrand base has m*nk elements; and consequently, there are 2m*nk possible truth assignments to consider. If we have 10 objects and 5 relation constants of arity 2, this means 2500 possibilities.

Fortunately, as with Propositional Logic, there are some shortcuts that allow us to analyze sentences in Relational Logic without examining all of these possibilities. In this chapter, we start with the truth table method and then look at some of these more efficient relational model checking methods.




Use the arrow keys to navigate.
Press the escape key to toggle all / one.