UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems

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. Green open access

[thumbnail of 1-s2.0-S2352220822000803-main.pdf]
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
Downloads since deposit
39Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item