The Taming of the Cut. Classical Refutations with Analytic Cut
From MaRDI portal
Publication:4304496
DOI10.1093/logcom/4.3.285zbMath0806.03037OpenAlexW1991138028MaRDI QIDQ4304496
Marco Mondadori, Marcello D'Agostino
Publication date: 16 February 1995
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/64c7e1602251f492e1104fcf758ec7cc1b640e33
complexitycut rulespeed-upanalytic tableauxalternative refutation system for classical logicclassical analytic deduction
Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Complexity of proofs (03F20)
Related Items
Informational semantics, non-deterministic matrices and feasible deduction, The enduring scandal of deduction. Is propositional logic really uninformative?, A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics, Analytic tableaux for non-deterministic semantics, CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT, Cut and pay, Correspondence analysis and automated proof-searching for first degree entailment, An epistemic operator for description logics, Semantics and proof-theory of depth bounded Boolean logics, Rasiowa-Sikorski deduction systems with the rule of cut: a case study, An Optimized KE-Tableau-Based System for Reasoning in the Description Logic $${\mathcal {DL}}_{{\mathbf {D}}}^{4,\!\times }$$, An informational view of classical logic, Abduction as deductive saturation: a proof-theoretic inquiry, Non-transitive correspondence analysis, A tableau proof system for a mazurkiewicz trace logic with fixpoints, Focusing in Linear Meta-logic, Labelling ideality and subideality, Fibred tableaux for multi-implication logics, Distributed modal theorem proving with KE, A tableau calculus for minimal model reasoning, The tableau-based theorem prover 3 T A P Version 4.0, Building decision procedures for modal logics from propositional decision procedures — The case study of modal K, Grammar specification in categorial logics and theorem proving, BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS, Optimization techniques for propositional intuitionistic logic and their implementation, 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, Hybrid-logical reasoning in the Smarties and Sally-Anne tasks, Using Abduction to Compute Efficient Proofs, A framework for proof systems, Non-distributive relatives of ETL and NFL, 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, Tableaux for logics of time and knowledge with interactions relating to synchrony, An efficient relational deductive system for propositional non-classical logics, Labelled proofs for quantified modal logic, A Set-theoretic Approach to Reasoning Services for the Description Logic 𝒟 ℒ D 4,×, An Improved Set-based Reasoner for the Description Logic 𝒟ℒD4,׆, The proof complexity of analytic and clausal tableaux, Chrysippus' logic in a natural deduction setting, Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\)., Using tableaux to automate the Lambek and other categorial calculi, Synthetic tableaux: Minimal tableau search heuristics, Unrestricted vs restricted cut in a tableau method for Boolean circuits
