A system of interaction and structure
From MaRDI portal
Publication:5277766
DOI10.1145/1182613.1182614zbMath1367.03110arXivcs/9910023OpenAlexW2102625227MaRDI QIDQ5277766
Publication date: 12 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/cs/9910023
symmetrycut eliminationlinear logicself-dualitynoncommutativitydeep inferencecalculus of structurespomset logicmix rule
Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Related Items
Power and Limits of Structural Display Rules, VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED, MELL in the calculus of structures, A Subatomic Proof System for Decision Trees, Behavioural Analysis of Sessions Using the Calculus of Structures, An Analytic Propositional Proof System on Graphs, A deep inference system for the modal logic S5, On the Power of Substitution in the Calculus of Structures, A Survey of the Proof-Theoretic Foundations of Logic Programming, When you must forget: Beyond strong persistence when forgetting in answer set programming, An intuitionistic formula hierarchy based on high‐school identities, Enumerating Independent Linear Inferences, A System of Interaction and Structure III: The Complexity of BV and Pomset Logic, On the Pre- and Promonoidal Structure of Spacetime, Non-crossing Tree Realizations of Ordered Degree Sequences, Realization for justification logics via nested sequents: modularity through embedding, On linear rewriting systems for Boolean logic and some applications to proof theory, A logical calculus for controlled monotonicity, On the decision problem for MELL, Linear Lambda Calculus and Deep Inference, A Logical Basis for Quantum Evolution and Entanglement, System BV is NP-complete, Maude as a Platform for Designing and Implementing Deep Inference Systems, A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs, Complexity of super-coherence problems in ASP, Hypersequent and display calculi -- a unified perspective, System NEL is Undecidable, Extension without cut, The three dimensions of proofs, Unnamed Item, Unnamed Item, Unnamed Item, On structuring proof search for first order linear logic, Composing dinatural transformations: towards a calculus of substitution, Scalable fine-grained proofs for formula processing, True Concurrency of Deep Inference Proofs, Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic, Deep Inference in Bi-intuitionistic Logic, Syntactic cut-elimination for common knowledge, Syntactic Cut-elimination for Common Knowledge, Deep inference and expansion trees for second-order multiplicative linear logic, Constructing weak simulations from linear implications for processes with private names, On linear logic planning and concurrency, From Schütte’s Formal Systems to Modern Automated Deduction, Pomset Logic, Canonical Abstract Syntax Trees, Prioritise the best variation, Cut elimination inside a deep inference system for classical predicate logic
