A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
From MaRDI portal
Publication:2095424
DOI10.1016/j.jlamp.2022.100827OpenAlexW3118620840WikidataQ115188990 ScholiaQ115188990MaRDI QIDQ2095424
Carlos Olarte, Elaine Pimentel, Camilo Rocha
Publication date: 16 November 2022
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2101.03113
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A note on harmony
- Linear logic
- Formal modeling: actors, open systems, biological systems. Essays dedicated to Carolyn Talcott on the occasion of her 70th birthday
- Deep sequent systems for modal logic
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Focusing and polarization in linear, intuitionistic, and classical logics
- Conditional rewriting logic as a unified model of concurrency
- A linear logical framework
- Theorem proving modulo
- Maude: specification and programming in rewriting logic
- Equational rules for rewriting logic
- Sequent systems for negative modalities
- Structural cut elimination. I: Intuitionistic and classical logic
- Twenty years of rewriting logic
- A formal framework for specifying sequent calculus proof systems
- Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1--4, 2020. Proceedings. Part II
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- A fresh view of linear logic as a logical framework
- Programming and symbolic computation in Maude
- Semantic foundations for generalized rewrite theories
- Built-in Variant Generation and Unification, and Their Applications in Maude 2.7
- Quati: An Automated Tool for Proving Permutation Lemmas
- Linear Nested Sequents, 2-Sequents and Hypersequents
- Proof Search in Nested Sequent Calculi
- Theorem Proving Modulo Based on Boolean Equational Procedures
- Logic Programming with Focusing Proofs in Linear Logic
- A framework for defining logics
- Modularisation of Sequent Calculi for Normal and Non-normal Modalities
- Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
- Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
- CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI
- Order-sorted Equational Unification Revisited
- Reflective metalogical frameworks
- An extended framework for specifying and reasoning about proof systems
- Eine Darstellung der Intuitionistischen Logik in der Klassischen
- Proving structural properties of sequent systems in rewriting logic
