Olarte, Carlos;
Pimentel, Elaine;
Rocha, Camilo;
(2023)
A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems.
Journal of Logical and Algebraic Methods in Programming
, 130
, Article 100827. 10.1016/j.jlamp.2022.100827.
Preview |
Text
1-s2.0-S2352220822000803-main.pdf - Published Version Download (908kB) | Preview |
Abstract
This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these structural properties are crucial in proof theory because they can reduce the proof-search effort and further be used as scaffolding for obtaining other meta-results such as consistency. The algorithms -- which take advantage of the rewriting logic meta-logical framework, and use rewrite- and narrowing-based reasoning -- are explained in detail and illustrated with examples throughout the paper. They have been fully mechanized in the L-Framework, thus offering both a formal specification language and off-the-shelf mechanization of the proof-search algorithms coming together with semi-decision procedures for proving theorems and meta-theorems of the object system. As illustrated with case studies in the paper, the L-Framework, achieves a great degree of automation when used on several propositional sequent systems, including single conclusion and multi-conclusion intuitionistic logic, classical logic, classical linear logic and its dyadic system, intuitionistic linear logic, and normal modal logics.
Type: | Article |
---|---|
Title: | A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems |
Open access status: | An open access version is available from UCL Discovery |
DOI: | 10.1016/j.jlamp.2022.100827 |
Publisher version: | https://doi.org/10.1016/j.jlamp.2022.100827 |
Language: | English |
Additional information: | © 2022 The Author(s). Published by Elsevier Inc. under a Creative Commons license (https://creativecommons.org/licenses/by/4.0/). |
Keywords: | Rewriting logic, Proof theory, Sequent systems |
UCL classification: | UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science UCL > Provost and Vice Provost Offices > UCL BEAMS UCL |
URI: | https://discovery.ucl.ac.uk/id/eprint/10158134 |
Archive Staff Only
View Item |