Although resolution-based inference is perhaps the industry standard in automated theorem proving, there have always been systems that employed a different format. For example, the Logic Theorist of 1957 produced proofs by using an axiomatic system, and the proofs it generated would be considered legitimate axiomatic proofs; Wang’s systems of the late 1950’s employed a Gentzen-sequent proof strategy; Beth’s systems written about the same time employed his semantic tableaux method; and Prawitz’s systems of again about the same time are often (...) said to employ a natural deduction format. [See Newell, et al (1957), Beth (1958), Wang (1960), and Prawitz et al (1960)]. Like sequent proof systems and tableaux proof systems, natural deduction systems retain.. (shrink)

The length of resolution proofs is investigated, relative to the model-theoretic measure of Herband complexity. A concept of resolution deduction is introduced which is somewhat more general than the classical concepts. It is shown that proof complexity is exponential in terms of Herband complexity and that this bound is tight. The concept of R-deduction is extended to FR-deduction, where, besides resolution, a function introduction rule is allowed. As an example, consider the clause P Q: conclude P) Q, where a, f (...) are new function symbols extending Herbrand's universe. P ()Q from Q) and Skolemization). By modification of a construction of Statman it is shown that FR-deductions may be nonelementarily shorter than R-deductions . Finally it is proved that FR-deduction has weaker effects only if clausal logic is restricted to Horn logic. (shrink)