Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
From MaRDI portal
Publication:1314288
DOI10.1007/BF00156916zbMath0793.03059OpenAlexW82633235MaRDI QIDQ1314288
Publication date: 10 March 1994
Published in: Journal of Logic, Language and Information (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00156916
Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Cut-elimination and normal-form theorems (03F05)
Related Items (23)
The universe of propositional approximations ⋮ A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics ⋮ Cut and pay ⋮ The SAT-based approach to separation logic ⋮ Semantics and proof-theory of depth bounded Boolean logics ⋮ Identifying Efficient Abductive Hypotheses Using Multicriteria Dominance Relation ⋮ On the Power of Substitution in the Calculus of Structures ⋮ Rasiowa-Sikorski deduction systems with the rule of cut: a case study ⋮ Abduction as deductive saturation: a proof-theoretic inquiry ⋮ Non-elementary speed-ups in proof length by different variants of classical analytic calculi ⋮ Building decision procedures for modal logics from propositional decision procedures — The case study of modal K ⋮ Towards an Efficient Prover for the <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si1.gif" overflow="scroll"><mml:msub><mml:mi>C</mml:mi><mml:mn>1</mml:mn></mml:msub></mml:math> Paraconsistent Logic ⋮ The Universe of Approximations ⋮ Non-distributive relatives of ETL and NFL ⋮ An empirical analysis of modal theorem provers ⋮ Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis ⋮ Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics ⋮ Normality, non-contamination and logical depth in classical natural deduction ⋮ Representing scope in intuitionistic deductions ⋮ Hybrid Tableaux for the Difference Modality ⋮ An efficient relational deductive system for propositional non-classical logics ⋮ Relative efficiency of propositional proof systems: Resolution vs. cut-free LK ⋮ Synthetic tableaux: Minimal tableau search heuristics
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Untersuchungen über das logische Schliessen. I
- Systematization of finite many-valued logics through the method of tableaux
- Towards feasible solutions of the tautology problem
- The relative efficiency of propositional proof systems
- Analytic cut
- The Unit Proof and the Input Proof in Theorem Proving
This page was built for publication: Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
