Hector Levesque e Ronald Brachman, A Fundamental Tradeoff in Knowledge Representation and Reasoning, in Ronald Brachman and Hector J. Levesque (a cura di), Readings in Knowledge Representation, Morgan Kaufmann, 1985, p. 49, ISBN 978-0-934613-01-9.
«The good news in reducing KR service to theorem proving is that we now have a very clear, very specific notion of what the KR system should do; the bad new is that it is also clear that the services can not be provided... deciding whether or not a sentence in FOL is a theorem... is unsolvable.»