Gentzen-type systems, resolution and tableaux
From MaRDI portal
Publication:1311413
DOI10.1007/BF00881838zbMath0788.03013OpenAlexW2007013614MaRDI QIDQ1311413
Publication date: 5 June 1994
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00881838
classical logicautomated deductioncutstransforming Gentzen-type derivations into resolution derivations
Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)
Related Items
A note on cut-elimination for classical propositional logic ⋮ Hypersequents, logical consequence and intermediate logics for concurrency ⋮ On Gentzen relations associated with finite-valued logics preserving degrees of truth ⋮ Paraconsistency, paracompleteness, Gentzen systems, and trivalent semantics ⋮ Cut elimination by unthreading ⋮ Abduction as deductive saturation: a proof-theoretic inquiry ⋮ Complementary proof nets for classical logic ⋮ GENERALITY AND EXISTENCE 1: QUANTIFICATION AND FREE LOGIC ⋮ A Multiple-Conclusion Calculus for First-Order Gödel Logic ⋮ Proof-terms for classical and intuitionistic resolution ⋮ Kripke Semantics for Basic Sequent Systems ⋮ Superposition with equivalence reasoning and delayed clause normal form transformation ⋮ Strict Canonical Constructive Systems ⋮ Canonical Signed Calculi, Non-deterministic Matrices and Cut-Elimination ⋮ GEOMETRISATION OF FIRST-ORDER LOGIC ⋮ A Strong Completeness Theorem for the Gentzen systems associated with finite algebras ⋮ Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi ⋮ FRACTIONAL SEMANTICS FOR CLASSICAL LOGIC ⋮ Abduction via C-tableaux and δ-resolution ⋮ What you always wanted to know about rigid E-unification ⋮ Relative efficiency of propositional proof systems: Resolution vs. cut-free LK ⋮ Two party immediate response disputes: Properties and efficiency
Cites Work
This page was built for publication: Gentzen-type systems, resolution and tableaux
