Deep inference and symmetry in classical proofs

MaRDI QIDQ3375282zbMATHFDO

Authors Kai Brünnler

Publication date 7 March 2006

zbMATH Keywords

proof searchdeep inferencenormalization of proof

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Classical propositional logic (03B05) Cut-elimination and normal-form theorems (03F05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Classical first-order logic (03B10) Structure of proofs (03F07)

Recommendations

• Locality for classical logic
• Logical Approaches to Computational Barriers
• Proof Complexity of the Cut-free Calculus of Structures
• A proof calculus which reduces syntactic bureaucracy
• A Local System for Classical Logic

Cited in

(18)

• A deep inference system for the modal logic S5
• On the proof complexity of deep inference
• Cut elimination inside a deep inference system for classical predicate logic
• Peirce's calculi for classical propositional logic
• Locality for classical logic
• On the length of medial-switch-mix derivations
• The three dimensions of proofs
• On the logical philosophy of assertive graphs
• A first order system with finite choice of premises
• On the proof complexity of cut-free bounded deep inference
• Deep sequent systems for modal logic
• From deep inference to proof nets via cut elimination
• Proof Complexity of the Cut-free Calculus of Structures
• Proof analysis of Peirce's alpha system of graphs
• A proof calculus which reduces syntactic bureaucracy
• The canonical pairs of bounded depth Frege systems
• Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
• Logical Approaches to Computational Barriers

This page was built for publication: Deep inference and symmetry in classical proofs

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