A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems

TL;DR

This paper presents a rewriting logic-based algorithmic approach for automating the proof of structural properties in propositional sequent systems, enhancing proof-search efficiency and enabling meta-theoretical reasoning.

Contribution

It introduces a formal, mechanized framework using rewriting logic and narrowing techniques for proving key proof-theoretic properties in various propositional logics.

Findings

Automated proof-search algorithms are effective across multiple propositional systems.

The L-Framework provides a formal language and mechanization for proof and meta-proof procedures.

Case studies demonstrate high automation and applicability to diverse logic systems.

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.