Geodesic
Monotone sequent calculus and resolution
Commentationes Mathematicae Universitatis Carolinae, Tome 42 (2001) no. 3, pp. 575-582

Voir la notice de l'article provenant de la source Czech Digital Mathematics Library

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.
Classification : 03B20, 03F07, 03F20, 03F55
Keywords: intuitionistic propositional logic; monotone logic; sequent calculus; resolution; complexity of proofs 
@article{CMUC_2001__42_3_a15,
     author = {B{\'\i}lkov\'a, Marta},
     title = {Monotone sequent calculus and resolution},
     journal = {Commentationes Mathematicae Universitatis Carolinae},
     pages = {575--582},
     publisher = {mathdoc},
     volume = {42},
     number = {3},
     year = {2001},
     mrnumber = {1860246},
     zbl = {1052.03037},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/CMUC_2001__42_3_a15/}
}
TY  - JOUR
AU  - Bílková, Marta
TI  - Monotone sequent calculus and resolution
JO  - Commentationes Mathematicae Universitatis Carolinae
PY  - 2001
SP  - 575
EP  - 582
VL  - 42
IS  - 3
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CMUC_2001__42_3_a15/
LA  - en
ID  - CMUC_2001__42_3_a15
ER  - 
%0 Journal Article
%A Bílková, Marta
%T Monotone sequent calculus and resolution
%J Commentationes Mathematicae Universitatis Carolinae
%D 2001
%P 575-582
%V 42
%N 3
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CMUC_2001__42_3_a15/
%G en
%F CMUC_2001__42_3_a15
Bílková, Marta. Monotone sequent calculus and resolution. Commentationes Mathematicae Universitatis Carolinae, Tome 42 (2001) no. 3, pp. 575-582. http://geodesic.mathdoc.fr/item/CMUC_2001__42_3_a15/