| << Prev | - Up - | Next >> |
In this chapter we will extend our tableaux calculus to first order logic. As we shall see, there're good reasons to do so: The boost in expressivity that comes with the move from propositional to first order logic allows us to cover a lot of interesting semantic phenomena that we couldn't handle before. But at the same time, this boost has certain less pleasant consequences - theoretically as well as practically. We lose the finite model property and decidability of satisfiability and theorem proving. This means that we have to take heavy measures to ensure termination in any implementation of a first-order inference system.
In the first part of this chapter, we will further motivate the extension of our tableaux calculus and give a theoretical overview of how the calculus has to be changed. In the second part, we will show how we practically handle these modifications (and the related problems) in our implementation.
Throughout this chapter, we will focus on model generation. Although the extended tableaux calculus can readily be used for theorem proving, we will not deeply discuss this issue here. The reason is that talking about first order theorem proving immediately gives rise to a discussion of efficency. Indeed there exists a whole literature on tuning tableaux calculi for efficient theorem proving. But this goes beyond what we want to do in this course.
| << Prev | - Up - | Next >> |