| Title:
|
Monotone sequent calculus and resolution (English) |
| Author:
|
Bílková, Marta |
| Language:
|
English |
| Journal:
|
Commentationes Mathematicae Universitatis Carolinae |
| ISSN:
|
0010-2628 (print) |
| ISSN:
|
1213-7243 (online) |
| Volume:
|
42 |
| Issue:
|
3 |
| Year:
|
2001 |
| Pages:
|
575-582 |
| . |
| Category:
|
math |
| . |
| Summary:
|
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. (English) |
| Keyword:
|
intuitionistic propositional logic |
| Keyword:
|
monotone logic |
| Keyword:
|
sequent calculus |
| Keyword:
|
resolution |
| Keyword:
|
complexity of proofs |
| MSC:
|
03B20 |
| MSC:
|
03F07 |
| MSC:
|
03F20 |
| MSC:
|
03F55 |
| idZBL:
|
Zbl 1052.03037 |
| idMR:
|
MR1860246 |
| . |
| Date available:
|
2009-01-08T19:16:19Z |
| Last updated:
|
2012-04-30 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/119272 |
| . |
| Reference:
|
[1] Atserias A., Galesi N., Gavalda R.: Monotone Proofs of the Pigeon Hole Principle.preprint, Barcelona University, 1999. Zbl 0989.03065, MR 1795891 |
| Reference:
|
[2] Atserias A., Galesi N., Pudlák P.: Monotone Simulations of Nonmonotone Propositional Proofs.ECCC Report TR00-087, 2000. |
| Reference:
|
[3] Cook S.A., Reckhow R.A.: The relative efficiency of propositional proof systems.J. Symbolic Logic 44 (1979), 36-50. Zbl 0408.03044, MR 0523487 |
| Reference:
|
[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. MR 1720576 |
| Reference:
|
[5] Takeuti G.: Proof Theory.North-Holland, second edition, 1987. Zbl 0681.03039, MR 0882549 |
| . |
