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
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
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
