Monotone sequent calculus and resolution. (English) Zbl 1052.03037

Three proof systems for propositional logic are briefly examined and compared, namely Monotonic Sequent Calculus (MLK), Intuitionistic Sequent Calculus (LJ), and Resolution, i.e.a refutation system for formulas in Conjunctive Normal Form. The complexity of a proof is measured by the number of proof steps, i.e.uses of rules. Using polynomial simulation between proofs, it is shown that monotone logic is a part of intuitionistic logic. Further, proving the pigeonhole principle and the clique principle are compared, showing that resolution is exponentially separated from MLK. The author also shows that if we have a resolution proof \(P\) from the set of monochromatic clauses, then there is an MLK proof \(Q\) (and consequently also an LJ proof) such that \(Q\) can be constructed in polynomial time from the resolution proof \(P\).


03F20 Complexity of proofs
Full Text: EuDML