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

Carlos Olarte, Elaine Pimentel, Camilo Rocha

Producción: Contribución a una revistaArtículorevisión exhaustiva

1 Cita (Scopus)


This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-admissibility, 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– 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.

Idioma originalInglés
Número de artículo100827
PublicaciónJournal of Logical and Algebraic Methods in Programming
EstadoPublicada - ene. 2023


Profundice en los temas de investigación de 'A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems'. En conjunto forman una huella única.

Citar esto