ISSN:
1573-7470
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
,
Mathematics
Notes:
Abstract Resolution and a cut-free Gentzen system are compared with respect to their efficiency as proof systems for biconditionals in the classical propositional calculus. The relative efficiency is shown to depend strongly on the proof format adopted. If proofs are represented as trees, then resolution can simulate the cut-free system efficiently, but an efficient reverse simulation is not possible. If proofs are represented as sequences, then efficient simulations are possible in both directions. The examples used to show this also show that regular cut-free Gentzen systems cannot simulate unrestricted cut-free Gentzen systems efficiently.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01531026
Permalink