arXiv subjects

Shay Allen Logan

Publications and source records attributed to Shay Allen Logan.

5 recordsLinked to original sources

arXiv2026

A Formal Framework for Noisy Runtime Verification

We introduce the logic EDMon---an epistemic dynamic logic meant to model monitorability concepts in noisy runtime verification. Its syntax and semantics are defined and explained and the connection between EDMon and monitorability and noisy runtime verification concepts is explored. We then demonstrate that EDMon is sufficient to capture many of the results in the noisy runtime verification literature and catalog its relation to nearby logics and describe a large class of its theorems.

cs.LO↗

arXiv2026

Hyperformalism for Relevant Modal Logics

The property of hyperformalism has proven to be a powerful tool in the analysis of relevant logics, revealing that increasingly weak relevant logics are closed under increasingly strong classes of non-uniform substitutions. In such substitutions, two instances of the same atom may be treated independently in virtue of syntactic features of their appearances in a complex. In this work, we extend the scope of hyperformalism to relevant modal logics by considering MPos-hyperformalism, that is, a property in which relevant modal logics are closed under substitutions in which nesting within the scope of modal operators is taken into account. We prove that the weak relevant modal logic B-Box is MPos-hyperformal and investigate the classes of non-uniform substitutions under which several extensions are closed. We then consider corresponding refinements of the variable sharing property that hold of such logics. We conclude by introducing a modal logic K-MPos that constitutes the largest MPos-hyperformal sublogic of the classical modal logic K and provide soundness and completeness results.

cs.LO↗

arXiv2026

Probabilistic Epistemic Dynamic Agentive Logic

I introduce PEDAL -- a probabilistic epistemic logic meant to capture, in propositional dynamic terms, the epistemic state of an agent engaged in checking whether a program meets its specification. Semantically, PEDAL is built `on top of' PDL and uses probability measures defined on the set of possible program valuations of an otherwise-specified PDL-model. A Hilbert system with one infinitary rule is provided and proved to be sound and complete. Near the end, I discuss possible ways to circumvent infinitary proof difficulties.

cs.LO↗

arXiv2024

Hyperformalism for Bunched Natural Deduction Systems

Logics closed under classes of substitutions broader than class of uniform substitutions are known as hyperformal logics. This paper extends known results about hyperformal logics in two ways. First: we examine a very powerful form of hyperformalism that tracks, for bunched natural deduction systems, essentially all the intensional content that can possibly be tracked. We demonstrate that, after a few tweaks, the well-known relevant logic $\mathbf{B}$ exhibits this form of hyperformalism. Second: we demonstrate that not only can hyperformalism be extended along these lines, it can also be extended to accommodate not just what is proved in a given logic but the proofs themselves. Altogether, the paper demonstrates that the space of possibilities for the study of hyperformalism is much larger than might have been expected.

math.LO↗

arXiv2024

Topics, Non-Uniform Substitutions, and Variable Sharing

The family of relevant logics can be faceted by a hierarchy of increasingly fine-grained variable sharing properties -- requiring that in valid entailments $A\to B$, some atom must appear in both $A$ and $B$ with some additional condition (e.g., with the same sign or nested within the same number of conditionals). In this paper, we consider an incredibly strong variable sharing property of lericone relevance that takes into account the path of negations and conditionals in which an atom appears in the parse trees of the antecedent and consequent. We show that this property of lericone relevance holds of the relevant logic $\mathbf{BM}$ (and that a related property of faithful lericone relevance holds of $\mathbf{B}$) and characterize the largest fragments of classical logic with these properties. Along the way, we consider the consequences for lericone relevance for the theory of subject-matter, for Logan's notion of hyperformalism, and for the very definition of a relevant logic itself.

math.LO↗