Por Carlos Olarte (LIPN, Université Sorbonne Paris Nord).
We develop 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 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 take advantage of the rewriting logic meta-logical framework, and use rewrite- and narrowing-based reasoning. 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, together with semi-decision procedures for proving theorems and meta-theorems of the object system. As illustrated with case studies, 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.
Joint work with Elaine Pimentel and Camilo Rocha.
Transmissão via Zoom.
