Comparison of Calculi for First Order Logic
Elmar Eder · 1992
From Chapter 1, we are now familiar with a couple of calculi which have a few common features. Namely, there is a notion of a derivation or proof (or refutation ) of a formula. A derivation D is a string over some fixed alphabet, or some object such as a tree that can easily be transformed to such a string representation. Now, the notion of a derivation always has the property that, for a given formula F and a given string D , it is decidable whether D is a derivation of F . And, in fact, in all calculi that we consider here, this is decidable in a time polynomial in the number of symbol occurrences of D . Moreover, a soundness- and completeness-theorem holds stating that a formula is valid (resp., unsatisfiable, in the case of refutation calculi) if and only if it has a derivation in the calculus.