4.2 Article

Defining Logical Systems via Algebraic Constraints on Proofs

Related references

Note: Only part of the references are listed.
Article Mathematics, Applied

From axioms to synthetic inference rules via focusing

Sonia Marin et al.

Summary: This paper examines the construction of synthetic inference rules using theories composed of bipolars. It explores the key step of transforming formulas into synthetic inference rules and demonstrates the flexibility of different approaches in this process.

ANNALS OF PURE AND APPLIED LOGIC (2022)

Proceedings Paper Computer Science, Software Engineering

Focused Proof-search in the Logic of Bunched Implications

Alexander Gheorghiu et al.

Summary: The paper introduces the notion of focusing principle to reformulate the traditional bunched sequent calculus in nested sequents, and proves that focused proof-search is complete for BI. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications.

FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2021 (2021)

Article Mathematics, Applied

Algebraic proof theory for substructural logics: Cut-elimination and completions

Agata Ciabattoni et al.

ANNALS OF PURE AND APPLIED LOGIC (2012)

Article Computer Science, Theory & Methods

Tableaux and Resource Graphs for Separation Logic

Didier Galmiche et al.

JOURNAL OF LOGIC AND COMPUTATION (2010)

Article Computer Science, Theory & Methods

Focusing and polarization in linear, intuitionistic, and classical logics

Chuck Liang et al.

THEORETICAL COMPUTER SCIENCE (2009)

Article Computer Science, Theory & Methods

The semantics of BI and resource tableaux

D Galmiche et al.

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE (2005)

Article Logic

Proof analysis in modal logic

S Negri

JOURNAL OF PHILOSOPHICAL LOGIC (2005)

Article Computer Science, Theory & Methods

Semantic labelled tableaux for propositional BI

D Galmiche et al.

JOURNAL OF LOGIC AND COMPUTATION (2003)

Article Mathematics

A proof-theoretic study of the correspondence of classical logic and modal logic

H Kushida et al.

JOURNAL OF SYMBOLIC LOGIC (2003)

Article Mathematics, Applied

On the semantics of classical disjunction

D Pym et al.

JOURNAL OF PURE AND APPLIED ALGEBRA (2001)

Article Computer Science, Theory & Methods

Efficient resource management for linear logic proof search

I Cervesato et al.

THEORETICAL COMPUTER SCIENCE (2000)

Article Computer Science, Theory & Methods

Internalizing labelled deduction

P Blackburn

JOURNAL OF LOGIC AND COMPUTATION (2000)