Methods and Calculi for Deduction
Wolfgang Bibel, Elmar Eder · 1993
Abstract Logic has been presented in David Israel’s Chapter as a language to formalize problems arising in subareas of intellectics (and of other fields, for that matter). In Davis’ Chapter, it is shown that logic also supplies a relationship (denoted by |=) among different statements (orformulas) in that language. Note that there are actually many logics in the literature. As a default, we meanfirst-order logic unless explicitly specified otherwise. The formulas related this way to the empty set of formulas (i.e.ϕ |= F) play a particularly important role. They are calledvalid formulas. It turns out that in many cases a problem can be reformulated as a logical formula to be proved valid. For this reason one often speaks of ‘theorem proving’ where in effect solving problems, as those just referred to, is the issue.