Logic Programming with Focusing Proofs in Linear Logic

DOI10.1093/LOGCOM/2.3.297zbMATH Open0764.03020OpenAlexW2070324762MaRDI QIDQ4018167FDOQ4018167

Authors: Jean-Marc Andreoli 

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

Recommendations

• Focussing and proof construction
• Logic programming in a fragment of intuitionistic linear logic
• Mechanizing focused linear logic in Coq
• Proofs as computations in linear logic
• On structuring proof search for first order linear logic

zbMATH Keywords

symmetryprogramming languageconcurrencyparallelismlogic programmingproof searchproof normalizationfocusing proofsabstract models of computationfragment of linear logicGentzen style sequent calculus for linear logicnormalization to clausal form

Mathematics Subject Classification ID

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
• Focused linear logic and the \(\lambda\)-calculus
• A linear logic framework for multimodal logics
• Subexponentials in non-commutative linear logic
• Structural focalization
• Subformula linking for intuitionistic logic with application to type theory
• Focused proof-search in the logic of bunched implications
• A sequent calculus for a semi-associative law
• Title not available (Why is that?)
• Cut elimination for the unified logic
• Implicational relevance logic is 2-\textsc{ExpTime}-complete
• 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
• A proposal for broad spectrum proof certificates
• Bracket induction for Lambek calculus with bracket modalities
• A general proof certification framework for modal logic
• Foundations for reliable and flexible interactive multimedia scores
• Representing scope in intuitionistic deductions
• Proof strategies in linear logic
• Non-commutative logic. III: Focusing proofs.
• Formalized meta-theory of sequent calculi for linear logics
• Modularity of proof-nets. Generating the type of a module.
• Linearity, control effects, and behavioral types
• On Lambek's restriction in the presence of exponential modalities
• Adjoint logic with a 2-category of modes
• A proof theoretic view of spatial and temporal dependencies in biochemical systems
• The multiplicative-additive Lambek calculus with subexponential and bracket modalities
• Hybridizing a logical framework
• Proof search and certificates for evidential transactions
• True concurrency semantics for a linear logic programming language with broadcast communication
• Mechanizing focused linear logic in Coq
• Logical approximation for program analysis
• The sequent calculus of skew monoidal categories
• Undecidability of multiplicative subexponential logic
• A proof theory for model checking: an extended abstract
• Connection-based proof construction in linear logic
• Programs with continuations and linear logic
• Call-By-Push-Value from a Linear Logic Point of View
• Tools for the investigation of substructural and paraconsistent logics
• A framework for linear authorization logics
• Title not available (Why is that?)
• Linear logic in computer science
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• A PSPACE-complete fragment of second-order linear logic
• A proof theory for model checking
• 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
• The ILLTP library for intuitionistic linear logic
• 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
• Resource-distribution via Boolean constraints (extended abstract)
• From axioms to synthetic inference rules via focusing
• 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 properties of concurrent computations in CLF
• Focused and Synthetic Nested Sequents
• MacNeille completions of FL-algebras
• A logical characterization of forward and backward chaining in the inverse method
• Title not available (Why is that?)
• Algebraic proof theory: hypersequents and hypercompletions
• Focussing and proof construction
• Proof checking and logic programming
• Proof checking and logic programming
• Multimodal linguistic inference
• Logic programming with sequent systems: a linear logic approach
• 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
• Computer Science Logic
• Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
• Soft subexponentials and multiplexing
• Logic programming in a fragment of intuitionistic linear logic
• Softness of MALL proof-structures and a correctness criterion with Mix
• Structure of proofs and the complexity of cut elimination

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)