Cut formulas in propositional logic
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.
- A direct proof of the equivalence between Brouwer's fan theorem and König's lemma with a uniqueness hypothesis
- A Machine-Oriented Logic Based on the Resolution Principle
- Bounds for proof-search and speed-up in the predicate calculus
- Cut elimination and automatic proof procedures
- The intractability of resolution
- The relative efficiency of propositional proof systems
This page was built for publication: Cut formulas in propositional logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q689298)
