Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents

Autor: Lyon, Tim S., Shillito, Ian, Tiu, Alwen

It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains in the model into a constant domain. This makes it a very challenging pro

Externí odkaz: http://arxiv.org/abs/2404.15855

A new calculus for intuitionistic Strong L\'ob logic: strong termination and cut-elimination, formalised

Autor: Shillito, Ian, van der Giessen, Iris, Goré, Rajeev, Iemhoff, Rosalie

We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong L\"ob logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A novel meas

Externí odkaz: http://arxiv.org/abs/2309.00486

Cut-Elimination for Provability Logic by Terminating Proof-Search

Autor: Gore, Rajeev, Ramanayake, Revantha, Shillito, Ian, Das, Anupam, Negri, S.

Publikováno v: Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021., 299-313
STARTPAGE=299;ENDPAGE=313;TITLE=Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021.
Lecture Notes in Computer Science ISBN: 9783030860585
TABLEAUX

Recently, Brighton gave another cut-admissibility proof for the standard set-based sequent calculus GLS for modal provability logic GL. One of the two induction measures that Brighton uses is novel: the maximum height of regress trees in an auxiliary

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c53262463b1ef0076a3069e74f7d78c7
https://hdl.handle.net/11370/deecd2d3-1560-4a2c-af42-ecf349a5cbe4

YOUR VIEWS.

Autor: Shillito, Ian, Goodwin, Peter, Eifler, Barbara, Ferguson, Lynn, Jungr, Barb, Hikk, Susan, Holofcener, Julia, Krupinski, Renny

Publikováno v: Stage; 3/23/2023, Issue 7387, p6-6, 2/3p