From axioms to synthetic inference rules via focusing
From MaRDI portal
Publication:2120974
DOI10.1016/j.apal.2022.103091OpenAlexW4206913075WikidataQ114682919 ScholiaQ114682919MaRDI QIDQ2120974
Elaine Pimentel, Marco Volpe, Sonia Marin, Dale A. Miller
Publication date: 1 April 2022
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.apal.2022.103091
Classical first-order logic (03B10) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions, Leśniewski's ontology -- proof-theoretic characterization
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A framework for proof systems
- Proof analysis in modal logic
- A logical characterization of forward and backward chaining in the inverse method
- Focusing and polarization in linear, intuitionistic, and classical logics
- Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
- Focussing and proof construction
- On structuring proof search for first order linear logic
- Uniform proofs as a foundation for logic programming
- GEOMETRISATION OF FIRST-ORDER LOGIC
- Hypersequent and Labelled Calculi for Intermediate Logics
- Proof Analysis
- Focused Labeled Proof Systems for Modal Logic
- Focusing and Polarization in Intuitionistic Logic
- Logic Programming with Focusing Proofs in Linear Logic
- Cut Elimination in the Presence of Axioms
- Hypersequents and Systems of Rules
- Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
- Focusing Strategies in the Sequent Calculus of Synthetic Connectives
- Proof analysis beyond geometric theories: from rule systems to systems of rules
- Logical Approaches to Computational Barriers
