Effizienzvergleiche von Beweisprozeduren

Zusammenfassung

Das Gebiet des automatischen Beweisens ist etwa seit 1965 zusehends unübersichtlicher geworden, da von Jahr zu Jahr neue Beweisprozeduren auftauchen, von denen die Autoren meistens behaupten, sie seien effizienter als die bis dahin bekannten Verfahren. Zur Begründung werden zwar nicht mehr die CPU-Zeiten von ein paar zufälligen Testbeispielen herangezogen, doch sehr viel überzeugender sind die Argumente oft auch heute noch nicht. Ausnahmen hiervon sind zum Beispiel die Arbeiten von KOWALSKI und KUEHNER [3] und LOVELAND [4], obwohl auch deren Vergleichsmethoden nicht allgemeiner Natur, sondern zugeschnitten sind auf die speziellen Verfahren, die dort verglichen werden.