definitive Beantwortung der Frage, ob ein bestimmter Satz aus einer Menge von Sätzen (Axiomen) folgt oder nicht. Insbesondere sucht man nach einem Algorithmus, der solche Entscheidungen leistet. Existiert ein derartiger Algorithmus, so nennt man die entsprechende Theorie entscheidbar, andernfalls unentscheidbar. Während die Aussagenlogik entscheidbar ist, ist die Prädikatenlogik nach