Cut formulas in propositional logic (Q689298)

Cut formulas in propositional logic can speed up some proofs exponentially (a cut-free system is used as reference when we talk about speed-ups); it is hence important to study proof systems with cut, types of cut formulas (atomic cuts versus general cuts) and also relations between cut and techniques which may speed up proofs. In Section 2, we try to explain the importance of atomic cut formulas. We study the resolution principle and analysis trees with atomic cut and conjecture that there are proofs by analysis trees with atomic cuts and refutations by resolution such that transferring them to cut-free proofs will cause exponential increase of the proof length. We also study unit resolution and conclude that transferring refutations by unit resolution to cut-free proofs does not cause exponential increase of the proof length. In Section 3, we discuss using definitions in analysis trees and in resolution. We conclude that it corresponds to using abbreviations in analysis trees and to adding possibilities to use more complicated cut formulas in resolution.