Logic Programming with Focusing Proofs in Linear Logic
From MaRDI portal
Publication:4018167
DOI10.1093/logcom/2.3.297zbMath0764.03020OpenAlexW2070324762MaRDI QIDQ4018167
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
symmetryparallelismlogic programmingconcurrencyprogramming languageproof 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) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Logic programming (68N17) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
Power and Limits of Structural Display Rules, Linear Logic Properly Displayed, On Lambek’s Restriction in the Presence of Exponential Modalities, Adjoint Logic with a 2-Category of Modes, A linear logic framework for multimodal logics, True concurrency semantics for a linear logic programming language with broadcast communication, Syntactic Completeness of Proper Display Calculi, An Analytic Propositional Proof System on Graphs, Weak units, universal cells, and coherence via universality for bicategories, A resource aware semantics for a focused intuitionistic calculus, Jump from parallel to sequential proofs: exponentials, A Survey of the Proof-Theoretic Foundations of Logic Programming, Proof Theory of Partially Normal Skew Monoidal Categories, A proof of the focusing theorem via MALL proof nets, An intuitionistic formula hierarchy based on high‐school identities, Elaborating dependent (co)pattern matching: No pattern left behind, Bracket induction for Lambek calculus with bracket modalities, Unnamed Item, Explorations in Subexponential Non-associative Non-commutative Linear Logic, Maximally multi-focused proofs for skew non-commutative \texttt{MILL}, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Focused linear logic and the \(\lambda\)-calculus, Unnamed Item, Unnamed Item, Focusing in Linear Meta-logic, Multi-focused cut elimination, Expressing additives using multiplicatives and subexponentials, An Isbell duality theorem for type refinement systems, A concurrent constraint programming interpretation of access permissions, Strong normalization for all-style LKtq, Extended Lambek Calculi and First-Order Linear Logic, TCC, with History, Correct Answers for First Order Logic, On the Relations between Disjunctive and Linear Logic Programming, Encryption as an abstract data-type, A Tableau Method for the Lambek Calculus based on a Matrix Characterization, Proof Checking and Logic Programming, Specifying Proof Systems in Linear Logic with Subexponentials, Proofs as computations in linear logic, Unnamed Item, Unnamed Item, Focused Inductive Theorem Proving, A phase semantics for polarized linear logic and second order conservativity, Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method, Unnamed Item, Least and Greatest Fixed Points in Linear Logic, On geometry of interaction for polarized linear logic, Unnamed Item, Unnamed Item, Unnamed Item, COCHIS: Stable and coherent implicits, Differential Linear Logic and Polarization, Axiom Directed Focusing, Ludics and Its Applications to Natural Language Semantics, Expanding the Realm of Systematic Proof Theory, Focalisation and Classical Realisability, Connection-based proof construction in linear logic, Resource-distribution via Boolean constraints, Hybrid linear logic, revisited, On the unification of classical, intuitionistic and affine logics, Subexponentials in non-commutative linear logic, Constructing weak simulations from linear implications for processes with private names, A general proof certification framework for modal logic, Unnamed Item, Towards Ludics Programming: Interactive Proof Search, Unnamed Item, The Sequent Calculus of Skew Monoidal Categories, A Linear Logic of Authorization and Knowledge, A focused linear logical framework and its application to metatheory of object logics, On concurrent behaviors and focusing in linear logic, From axioms to synthetic inference rules via focusing, Cut elimination for the unified logic, Softness of MALL proof-structures and a correctness criterion with Mix, Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), Structure of proofs and the complexity of cut elimination, MELL in the calculus of structures, The sequent calculus of skew monoidal categories, Proof strategies in linear logic, On proof normalization in linear logic, First-order linear logic without modalities is NEXPTIME-hard, Proof checking and logic programming, A proof theoretic view of spatial and temporal dependencies in biochemical systems, A focus system for the alternation-free \(\mu \)-calculus, From Focalization of Logic to the Logic of Focalization, Coherence via focusing for symmetric skew monoidal categories, IMPLICATIONAL RELEVANCE LOGIC IS 2-EXPTIME-COMPLETE, Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols, Hypersequent rules with restricted contexts for propositional modal logics, A unified procedure for provability and counter-model generation in minimal implicational logic, A categorical semantics for polarized MALL, A Linear Logic Programming Language for Concurrent Programming over Graph Structures, A Proof Theoretic Study of Soft Concurrent Constraint Programming, On subexponentials, focusing and modalities in concurrent systems, Tools for the Investigation of Substructural and Paraconsistent Logics, Multimodal linguistic inference, Entailment-based actions for coordination, Foundations for Reliable and Flexible Interactive Multimedia Scores, A game semantics for disjunctive logic programming, Structural Focalization, Logical approximation for program analysis, Figures of dialogue: a view from ludics, Algebraic proof theory for substructural logics: cut-elimination and completions, Subexponential concurrent constraint programming, Formalized meta-theory of sequent calculi for linear logics, Parsing/theorem-proving for logical grammar \textit{CatLog3}, Linear logic in computer science, A semantic framework for proof evidence, Resource modalities in tensor logic, Proof and refutation in MALL as a game, A focused approach to combining logics, A rewriting framework and logic for activities subject to regulations, First-order automated reasoning with theories: when deduction modulo theory meets practice, From QBFs to \textsf{MALL} and back via focussing, A PSPACE-complete fragment of second-order linear logic, MacNeille completions of FL-algebras, Non-commutative logic. III: Focusing proofs., A framework for linear authorization logics, Linearity, Control Effects, and Behavioral Types, An Indexed System for Multiplicative Additive Polarized Linear Logic, A logical characterization of forward and backward chaining in the inverse method, A fresh view of linear logic as a logical framework, Focused proof-search in the logic of bunched implications, Forum: A multiple-conclusion specification logic, Proof nets for classical logic, Proof certificates for equality reasoning, Multi-focused proofs with different polarity assignments, From cut-free calculi to automated deduction: the case of bounded contraction, Hybrid and subexponential linear logics, The polarized \(\lambda\)-calculus, Kripke semantics for higher-order type theory applied to constraint logic programming languages, Proving concurrent constraint programming correct, revisited, Preface to the special volume, On the unity of duality, Linearizing intuitionistic implication, Hypersequent and display calculi -- a unified perspective, Modularity of proof-nets. Generating the type of a module., Resolution is cut-free, A framework for proof systems, On structuring proof search for first order linear logic, Non-commutative proof construction: a constraint-based approach, Algebraic proof theory: hypersequents and hypercompletions, The multiplicative-additive Lambek calculus with subexponential and bracket modalities, Call-By-Push-Value from a Linear Logic Point of View, Verification of spatial and temporal modalities in biochemical systems, Focused and Synthetic Nested Sequents, On the Meaning of Focalization, Subformula linking for intuitionistic logic with application to type theory, Proof search and certificates for evidential transactions, Representing scope in intuitionistic deductions, Permutability of proofs in intuitionistic sequent calculi, A Proposal for Broad Spectrum Proof Certificates, Focusing and polarization in linear, intuitionistic, and classical logics, Encoding Generic Judgments, Connection methods in linear logic and proof nets construction, Cut-elimination for a logic with definitions and induction, Proof-search in type-theoretic languages: An introduction, On linear logic planning and concurrency, Game of grounds, Focussing and proof construction, A proof theory for model checking, An interpretation of CCS into ludics, Formal meta-level analysis framework for quantum programming languages, Mechanizing focused linear logic in Coq, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, Soft subexponentials and multiplexing, Hybridizing a Logical Framework, Rewritings for Polarized Multiplicative and Exponential Proof Structures, Specifying Properties of Concurrent Computations in CLF, Resourceful program synthesis from graded linear types
