Automated Theorem Proving

While model checking as an automatized procedure has appeared not before the 1980s automated theorem proving was already there when the first computers have been available^2.3.

Despite the fact that the automated procedures for automated theorem proving are meanwhile quite sophisticated and powerful all these formal logic approaches suffer nevertheless from at least one difficulty: while the interpretation $I$ of some formal expression $f$ of a formal language $S$ is usual 'intuitively directly understandable' (operational!), the formal inference rules of a formal logic and much less the complex application of many inference rules in a sequence are usually rather 'not intuitiv', not 'directly controllable'. To 'check' an automatic inference directly is usually completely impossible^2.4. This is a real drawback of formal inferences. There are also other issues like 'undecidability' on account of too expressive languages or the principal asymmetry of 'provability' and 'satisfyability' according Godel 1931 [117] and later Tarski 1935 [264]: a formal system which is eqivalent or stronger than first order logic is either 'correct' and 'not complete' or 'complete' and 'not correct'. This means not all 'semantically true' expressions can be covered by a formally correct system. Furthermore are those systems not decidable in all cases (Turing 1936/7 [274]).

From this does not automatically follow that model checking is in every case better. Model checking has its inherent problems too. But to use formal logic with automated theorem proving and an appropriate meaning than both approaches could be possible witin certain limits.