Methods of cut-elimination

DOI10.1007/978-94-007-0320-9MaRDI QIDQ609451zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(38)

• Hybrid-logical reasoning in the Smarties and Sally-Anne tasks
• On the completeness of interpolation algorithms
• scientific article; zbMATH DE number 1471986 (Why is no real title available?)
• Cut Elimination for First Order Gödel Logic by Hyperclause Resolution
• scientific article; zbMATH DE number 7580067 (Why is no real title available?)
• Don't eliminate cut
• Cut-elimination: syntax and semantics
• Reducing redundancy in cut-elimination by resolution
• Simulating strong practical proof systems with extended resolution
• Herbrand's theorem in inductive proofs
• Schematic cut elimination and the ordered pigeonhole principle
• CERES for first-order schemata
• Logic for Programming, Artificial Intelligence, and Reasoning
• The logicality of equality
• Ceres in intuitionistic logic
• Complexity of translations from resolution to sequent calculus
• Epsilon calculus provides shorter cut-free proofs
• Efficient interpolation beyond cut-free proofs: admissible cuts and optimized extraction
• Cut Elimination In Situ
• Fast cut-elimination by CERES
• Craig interpolation with clausal first-order tableaux
• Cutting Out Continuations
• Schematic refutations of formula schemata
• On interpolation in automated theorem proving
• A complete tableau system for basic hybrid logic with propositional quantification
• Logic for Programming, Artificial Intelligence, and Reasoning
• The elimination of atomic cuts and the semishortening property for Gentzen's sequent calculus with equality
• First-order interpolation derived from propositional interpolation
• Extracting Herbrand systems from refutation schemata
• scientific article; zbMATH DE number 2006630 (Why is no real title available?)
• Herbrand analyses in geometry: a case study
• A Clausal Approach to Proof Analysis in Second-Order Logic
• Extraction of expansion trees
• On the convergence of reduction-based and model-based methods in proof theory
• Proof Transformation by CERES
• 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)