Logic Programming with Focusing Proofs in Linear Logic
From MaRDI portal
Publication:4018167
DOI10.1093/LOGCOM/2.3.297zbMATH Open0764.03020OpenAlexW2070324762MaRDI QIDQ4018167FDOQ4018167
Publication date: 16 January 1993
Published in: Journal Of Logic And Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/b9dd97a9ed29263923a2d7da195f1f7e790242d1
symmetryprogramming languageconcurrencyparallelismlogic programmingproof searchproof normalizationfocusing proofsabstract models of computationfragment of linear logicGentzen style sequent calculus for linear logicnormalization to clausal form
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Cut-elimination and normal-form theorems (03F05) Logic programming (68N17) Subsystems of classical logic (including intuitionistic logic) (03B20) Logic in computer science (03B70)
Cited In (only showing first 100 items - show all)
- A fresh view of linear logic as a logical framework
- From QBFs to \textsf{MALL} and back via focussing
- Focused linear logic and the \(\lambda\)-calculus
- A linear logic framework for multimodal logics
- Subexponentials in non-commutative linear logic
- Adjoint Logic with a 2-Category of Modes
- On Lambek’s Restriction in the Presence of Exponential Modalities
- Subformula linking for intuitionistic logic with application to type theory
- Focused proof-search in the logic of bunched implications
- The Sequent Calculus of Skew Monoidal Categories
- Title not available (Why is that?)
- Cut elimination for the unified logic
- An interpretation of CCS into ludics
- Formal meta-level analysis framework for quantum programming languages
- Syntactic Completeness of Proper Display Calculi
- On subexponentials, focusing and modalities in concurrent systems
- Resourceful program synthesis from graded linear types
- From cut-free calculi to automated deduction: the case of bounded contraction
- Hybrid and subexponential linear logics
- Multi-focused proofs with different polarity assignments
- The polarized \(\lambda\)-calculus
- Focused Inductive Theorem Proving
- Title not available (Why is that?)
- Bracket induction for Lambek calculus with bracket modalities
- Non-commutative logic. III: Focusing proofs.
- Weak units, universal cells, and coherence via universality for bicategories
- Structural Focalization
- Formalized meta-theory of sequent calculi for linear logics
- Modularity of proof-nets. Generating the type of a module.
- IMPLICATIONAL RELEVANCE LOGIC IS 2-EXPTIME-COMPLETE
- A proof theoretic view of spatial and temporal dependencies in biochemical systems
- Coherence via focusing for symmetric skew monoidal categories
- The multiplicative-additive Lambek calculus with subexponential and bracket modalities
- Hybridizing a logical framework
- Foundations for Reliable and Flexible Interactive Multimedia Scores
- Title not available (Why is that?)
- Proof search and certificates for evidential transactions
- A Proposal for Broad Spectrum Proof Certificates
- True concurrency semantics for a linear logic programming language with broadcast communication
- Mechanizing focused linear logic in Coq
- Logical approximation for program analysis
- Connection-based proof construction in linear logic
- Resource-distribution via Boolean constraints
- Linearity, Control Effects, and Behavioral Types
- Call-By-Push-Value from a Linear Logic Point of View
- Linear Logic Properly Displayed
- A framework for linear authorization logics
- Title not available (Why is that?)
- Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
- A PSPACE-complete fragment of second-order linear logic
- A resource aware semantics for a focused intuitionistic calculus
- Game of grounds
- A semantic framework for proof evidence
- Proof Theory of Partially Normal Skew Monoidal Categories
- Proof certificates for equality reasoning
- Title not available (Why is that?)
- Title not available (Why is that?)
- Connection methods in linear logic and proof nets construction
- Proof-search in type-theoretic languages: An introduction
- Proof nets for classical logic
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
- Tools for the Investigation of Substructural and Paraconsistent Logics
- From axioms to synthetic inference rules via focusing
- A Proof Theoretic Study of Soft Concurrent Constraint Programming
- A rewriting framework and logic for activities subject to regulations
- Kripke semantics for higher-order type theory applied to constraint logic programming languages
- Proving concurrent constraint programming correct, revisited
- A categorical semantics for polarized MALL
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- A framework for proof systems
- Parsing/theorem-proving for logical grammar \textit{CatLog3}
- Least and Greatest Fixed Points in Linear Logic
- Figures of dialogue: a view from ludics
- Proofs as computations in linear logic
- Title not available (Why is that?)
- Resource modalities in tensor logic
- Entailment-based actions for coordination
- Algebraic proof theory for substructural logics: cut-elimination and completions
- Non-commutative proof construction: a constraint-based approach
- Linearizing intuitionistic implication
- Specifying Proof Systems in Linear Logic with Subexponentials
- Specifying properties of concurrent computations in CLF
- Encryption as an abstract data-type
- Focused and Synthetic Nested Sequents
- Title not available (Why is that?)
- MacNeille completions of FL-algebras
- A general proof certification framework for modal logic
- A logical characterization of forward and backward chaining in the inverse method
- Algebraic proof theory: hypersequents and hypercompletions
- Representing scope in intuitionistic deductions
- Focussing and proof construction
- Proof checking and logic programming
- Proof strategies in linear logic
- Power and Limits of Structural Display Rules
- Multimodal linguistic inference
- A concurrent constraint programming interpretation of access permissions
- Forum: A multiple-conclusion specification logic
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
- Extended Lambek Calculi and First-Order Linear Logic
This page was built for publication: Logic Programming with Focusing Proofs in Linear Logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4018167)
