10.1.4 Rule-like World Knowledge and Computational Nightmares

Explanation why first order inference is undecidable.

Something we could not deal with using the methods from Section 7.2 was knowledge like ``Every man has a father''. In full first-order logic, such knowledge is very easy to write down:

But in a calculus such formulas are as dangerous as they're useful. To understand why, let's look at a tableaux constructed from our father-son-rule and the fact .

-Constellation

What's happening here? Intuitively, our tableaux is generating and endless chain of fathers: John is a man, therefore he has a father. The father is a man as well and therefore he also has father who is a man again... . More formally, the pattern is as follows: The universal quantification is instantiated. This directly results in an implication, which is expanded next. While one of the resulting branches closes immediately, we get an existential quantification on the other one. And here we get into trouble. We have to introduce a new constant - but now we have got all it takes to produce exactly the same constellation again. We can re-instantiate the universal quantification (with our new constant) and finally get a new existential quantification, giving us a third constant etc. The crucial point is that we can go on like this forever. We can always produce new constants, allowing us to re-apply the universal rule indefinitely. We call such a pattern a -constellation .



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