Zobrazeno 1 - 10
of 43
pro vyhledávání: '"Lyon, Tim S."'
Autor:
Lyon, Tim S.
We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for G\"odel-L\"ob provability logic. In particular, we consider Sambin and Valentini's sequent system GLseq, Shamkanov's non-wellfounded and cyclic
Externí odkaz:
http://arxiv.org/abs/2410.24053
Autor:
Lyon, Tim S.
We define and study translations between the maximal class of analytic display calculi for tense logics and labeled sequent calculi, thus solving an open problem about the translatability of proofs between the two formalisms. In particular, we provid
Externí odkaz:
http://arxiv.org/abs/2406.19882
The decidability of axiomatic extensions of the modal logic K with modal reduction principles, i.e. axioms of the form $\Diamond^{k} p \rightarrow \Diamond^{n} p$, has remained a long-standing open problem. In this paper, we make significant progress
Externí odkaz:
http://arxiv.org/abs/2405.10094
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
Autor:
Lyon, Tim S., Karge, Jonas
We introduce a constructive method applicable to a large number of description logics (DLs) for establishing the concept-based Beth definability property (CBP) based on sequent systems. Using the highly expressive DL RIQ as a case study, we introduce
Externí odkaz:
http://arxiv.org/abs/2404.15840
Autor:
Lyon, Tim S., van Berkel, Kees
This paper provides a set of cut-free complete sequent-style calculi for deontic STIT ('See To It That') logics used to formally reason about choice-making, obligations, and norms in a multi-agent setting. We leverage these calculi to write a proof-s
Externí odkaz:
http://arxiv.org/abs/2402.03148
Autor:
Lyon, Tim S., Ciabattoni, Agata, Galmiche, Didier, Larchey-Wendling, Dominique, Méry, Daniel, Olivetti, Nicola, Ramanayake, Revantha
This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing
Externí odkaz:
http://arxiv.org/abs/2312.03426
Autor:
Lyon, Tim S., Rudolph, Sebastian
This paper establishes alternative characterizations of very expressive classes of existential rule sets with decidable query entailment. We consider the notable class of greedy bounded-treewidth sets (gbts) and a new, generalized variant, called wea
Externí odkaz:
http://arxiv.org/abs/2307.08481
Autor:
Lyon, Tim S., Orlandelli, Eugenio
This paper studies nested sequents for quantified modal logics. In particular, it considers extensions of the propositional modal logics definable by the axioms D, T, B, 4, and 5 with varying, increasing, decreasing, and constant domains. Each calcul
Externí odkaz:
http://arxiv.org/abs/2307.08032
Autor:
Lyon, Tim S.
We present nested sequent systems for propositional G\"odel-Dummett logic and its first-order extensions with non-constant and constant domains, built atop nested calculi for intuitionistic logics. To obtain nested systems for these G\"odel-Dummett l
Externí odkaz:
http://arxiv.org/abs/2306.07550