A framework for proof systems

DOI10.1007/s10817-010-9182-1zbMath1242.03057OpenAlexW2020595717MaRDI QIDQ707742

Vivek Nigam, Dale A. Miller

Publication date: 8 October 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-010-9182-1

zbMATH Keywords

linear logicfocusinglogical frameworkmeta-logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

On concurrent behaviors and focusing in linear logic, From axioms to synthetic inference rules via focusing, A linear logic framework for multimodal logics, On subexponentials, focusing and modalities in concurrent systems, Subexponential concurrent constraint programming, Explorations in Subexponential Non-associative Non-commutative Linear Logic, A rewriting framework and logic for activities subject to regulations, Unnamed Item, A framework for linear authorization logics, A fresh view of linear logic as a logical framework, Multi-focused cut elimination, Multi-focused proofs with different polarity assignments, Yet another bijection between sequent calculus and natural deduction, Proving concurrent constraint programming correct, revisited, Hybrid linear logic, revisited, Mechanizing focused linear logic in Coq, Soft subexponentials and multiplexing, Non-associative, non-commutative multi-modal linear logic, A focused linear logical framework and its application to metatheory of object logics

Uses Software

• Pesca
• Elf
• Lolli

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• A minimal classical sequent calculus free of structural rules
• Forum: A multiple-conclusion specification logic
• A logical characterization of forward and backward chaining in the inverse method
• Focusing and polarization in linear, intuitionistic, and classical logics
• Logic programming in a fragment of intuitionistic linear logic
• Hypersequents, logical consequence and intermediate logics for concurrency
• Natural deduction with general elimination rules
• Normal natural deduction proofs (in classical logic)
• The foundation of a generic theorem prover
• Non-commutative logic. I: The multiplicative fragment
• Uniform proofs as a foundation for logic programming
• The Mathematics of Sentence Structure
• Focusing in Linear Meta-logic
• Incorporating Tables into Proofs
• A natural extension of natural deduction
• Logic Programming with Focusing Proofs in Linear Logic
• A framework for defining logics
• The Taming of the Cut. Classical Refutations with Analytic Cut
• On the Specification of Sequent Systems
• Analytic cut
• A formulation of the simple theory of types
• Eine Darstellung der Intuitionistischen Logik in der Klassischen
• Logical Approaches to Computational Barriers