Monotone sequent calculus and resolution

Marta Bílková

Commentationes Mathematicae Universitatis Carolinae (2001)

  • Volume: 42, Issue: 3, page 575-582
  • ISSN: 0010-2628

Abstract

top
We study relations between propositional Monotone Sequent Calculus (MLK --- also known as Geometric Logic) and Resolution with respect to the complexity of proofs, namely to the concept of the polynomial simulation of proofs. We consider Resolution on sets of monochromatic clauses. We prove that there exists a polynomial simulation of proofs in MLK by intuitionistic proofs. We show a polynomial simulation between proofs from axioms in MLK and corresponding proofs of contradiction (refutations) in MLK. Then we show a relation between a resolution refutation of a set of monochromatic clauses (CNF formula) and a proof of the sequent (representing corresponding DNF formula) in MLK. Because monotone logic is a part of intuitionistic logic, results are relevant for intuitionistic logic too.

How to cite

top

Bílková, Marta. "Monotone sequent calculus and resolution." Commentationes Mathematicae Universitatis Carolinae 42.3 (2001): 575-582. <http://eudml.org/doc/248791>.

@article{Bílková2001,
abstract = {We study relations between propositional Monotone Sequent Calculus (MLK --- also known as Geometric Logic) and Resolution with respect to the complexity of proofs, namely to the concept of the polynomial simulation of proofs. We consider Resolution on sets of monochromatic clauses. We prove that there exists a polynomial simulation of proofs in MLK by intuitionistic proofs. We show a polynomial simulation between proofs from axioms in MLK and corresponding proofs of contradiction (refutations) in MLK. Then we show a relation between a resolution refutation of a set of monochromatic clauses (CNF formula) and a proof of the sequent (representing corresponding DNF formula) in MLK. Because monotone logic is a part of intuitionistic logic, results are relevant for intuitionistic logic too.},
author = {Bílková, Marta},
journal = {Commentationes Mathematicae Universitatis Carolinae},
keywords = {intuitionistic propositional logic; monotone logic; sequent calculus; resolution; complexity of proofs; complexity of proofs; monotone logic; intuitionistic propositional logic; sequent calculus; resolution},
language = {eng},
number = {3},
pages = {575-582},
publisher = {Charles University in Prague, Faculty of Mathematics and Physics},
title = {Monotone sequent calculus and resolution},
url = {http://eudml.org/doc/248791},
volume = {42},
year = {2001},
}

TY - JOUR
AU - Bílková, Marta
TI - Monotone sequent calculus and resolution
JO - Commentationes Mathematicae Universitatis Carolinae
PY - 2001
PB - Charles University in Prague, Faculty of Mathematics and Physics
VL - 42
IS - 3
SP - 575
EP - 582
AB - We study relations between propositional Monotone Sequent Calculus (MLK --- also known as Geometric Logic) and Resolution with respect to the complexity of proofs, namely to the concept of the polynomial simulation of proofs. We consider Resolution on sets of monochromatic clauses. We prove that there exists a polynomial simulation of proofs in MLK by intuitionistic proofs. We show a polynomial simulation between proofs from axioms in MLK and corresponding proofs of contradiction (refutations) in MLK. Then we show a relation between a resolution refutation of a set of monochromatic clauses (CNF formula) and a proof of the sequent (representing corresponding DNF formula) in MLK. Because monotone logic is a part of intuitionistic logic, results are relevant for intuitionistic logic too.
LA - eng
KW - intuitionistic propositional logic; monotone logic; sequent calculus; resolution; complexity of proofs; complexity of proofs; monotone logic; intuitionistic propositional logic; sequent calculus; resolution
UR - http://eudml.org/doc/248791
ER -

References

top
  1. Atserias A., Galesi N., Gavalda R., Monotone Proofs of the Pigeon Hole Principle, preprint, Barcelona University, 1999. Zbl0989.03065MR1795891
  2. Atserias A., Galesi N., Pudlák P., Monotone Simulations of Nonmonotone Propositional Proofs, ECCC Report TR00-087, 2000. 
  3. Cook S.A., Reckhow R.A., The relative efficiency of propositional proof systems, J. Symbolic Logic 44 (1979), 36-50. (1979) Zbl0408.03044MR0523487
  4. Pudlák, P., On the complexity of the propositional calculus, in Sets and Proofs, Invited papers from Logic Colloquium 1997, S.B. Cooper and J.K. Truss eds., Cambridge University Press, 1999, pp. 197-218. MR1720576
  5. Takeuti G., Proof Theory, North-Holland, second edition, 1987. Zbl0681.03039MR0882549

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.