Cut formulas in propositional logic

DOI10.1016/0304-3975(93)90249-SMaRDI QIDQ689298zbMATH OpenOpenAlexFDO

Authors Wenhui Zhang

Publication date 20 December 1993

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(93)90249-s

zbMATH Keywords

propositional logicresolution principleproof lengthspeed upanalysis treesatomic cutcut formulascut-free proofs

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Recommendations

• Analytic cut trees
• Cut Elimination In Situ
• Structure of proofs and the complexity of cut elimination
• Cut elimination and automatic proof procedures
• Relative efficiency of propositional proof systems: Resolution vs. cut-free LK

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A direct proof of the equivalence between Brouwer's fan theorem and König's lemma with a uniqueness hypothesis
• 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

Cited in

(5)

• From the subformula property to cut-admissibility in propositional sequent calculi
• Relative efficiency of propositional proof systems: Resolution vs. cut-free LK
• Cut for core logic
• Cut and Weakening in Fuzzy Horn Logic
• A Subatomic Proof System for Decision Trees

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)