Relative Efficiency of Nonclassical Resolution and Cut-free Sequent System
Abstract
Comparison of the efficiency of resolution system and cut-free sequent calculus remains an open problem since 1974 (Cook, Reckhow). The problem was solved by A. Chubaryan for classical propositional logic in 2001. The paper proves that mentioned two systems for Intuitionistic propositional logic (Minimal propositional logic) are also polynomially equivalent.
References
P. Pudlák, The Lengths of Proofs, Handbook of proof theory, North-Holland, 1998, 547-637.
S.C. Klene, Introduction to metamathematics, D. Van Nostrand Company, INC, New York, 1952.
An. Chubaryan, Arm. Chubaryan, S. Sayadyan, The relative officiency of propositional proofs systems for classical and nonclassical logic, Fisrt conference of UNILOG-05, Hand-book, Montreux, 2005, 94.
S.A. Cook, A.R. Reckhow, Relative efficiency of propositional proof systems, JSL 44, 1, 1979, 36-50.
G.Mints, Resolution systems for nonclassical logic, Semiotika I informatika, vip. 25, 1985, 120-133 (in Russian).
U. Egly, S. Schmitt, On Intuitionistic Proof Transformations, their Complexity, and Application to Constructive Program Synthesis, Forschungrbericht AIDA-99-02, Darmstadt, Germany, 2003, 43-68.
H. Bolibekyan, A. Chubaryan, On some proof systems for I. Johansson's minimal logic of predicates, Logic Colloquium 2003, Helsinki, Finland, Aug. 14-20, 2003, Abstracts, p.56.
A. A. Chubaryan, Relative efficiency of a proof systems of classical propositional logic, Izvestija Natsionalnoj Akademii Nauk Armenii, Matematica, Vol. 37, N5, 2002, 45-58. [English translation: Jornal of Contemporary Mathematical Analysis (Armenian Academy of Sciences), Vol. 37, N5].
Downloads
Published
How to Cite
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
