Methods of cut-elimination

DOI10.1007/978-94-007-0320-9zbMATH Open1225.03075OpenAlexW619146373MaRDI QIDQ609451FDOQ609451

Authors: Matthias Baaz, Alexander Leitsch 

Publication date: 30 November 2010

Published in: Trends in Logic -- Studia Logica Library (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-94-007-0320-9

Recommendations

• Cut-elimination: syntax and semantics
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• Towards a clausal analysis of cut-elimination
• Cut Elimination for First Order Gödel Logic by Hyperclause Resolution

zbMATH Keywords

resolutioncut-eliminationmethod CERES

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) Mechanization of proofs and logical operations (03B35)

Cited In (31)

• Hybrid-logical reasoning in the Smarties and Sally-Anne tasks
• Title not available (Why is that?)
• Cut Elimination for First Order Gödel Logic by Hyperclause Resolution
• Title not available (Why is that?)
• Don't eliminate cut
• Cut-elimination: syntax and semantics
• Reducing redundancy in cut-elimination by resolution
• Simulating strong practical proof systems with extended resolution
• Schematic cut elimination and the ordered pigeonhole principle
• CERES for first-order schemata
• Logic for Programming, Artificial Intelligence, and Reasoning
• The logicality of equality
• Complexity of translations from resolution to sequent calculus
• Ceres in intuitionistic logic
• Cut Elimination In Situ
• Fast cut-elimination by CERES
• Craig interpolation with clausal first-order tableaux
• Cutting Out Continuations
• Schematic refutations of formula schemata
• Logic for Programming, Artificial Intelligence, and Reasoning
• On interpolation in automated theorem proving
• The elimination of atomic cuts and the semishortening property for Gentzen's sequent calculus with equality
• Title not available (Why is that?)
• First-order interpolation derived from propositional interpolation
• A Clausal Approach to Proof Analysis in Second-Order Logic
• On the convergence of reduction-based and model-based methods in proof theory
• Proof Transformation by CERES
• Extraction of expansion trees
• Effective Skolemization
• Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts
• PROOF-THEORETIC ANALYSIS OF THE QUANTIFIED ARGUMENT CALCULUS

This page was built for publication: Methods of cut-elimination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q609451)