Tootfinder

LeanLTL: A unifying framework for linear temporal logics in Lean
Eric Vin, Kyle A. Miller, Daniel J. Fremont
https://arxiv.org/abs/2507.01780 https://

LeanLTL: A unifying framework for linear temporal logics in Lean
We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a wa…

Coalgebraic proof translations for non-wellfounded proofs
Borja Sierra Miranda, Thomas Studer, Lukas Zenger
https://arxiv.org/abs/2506.01711 https://

Coalgebraic proof translations for non-wellfounded proofs
Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely well-founded frame conditions like GL or Grz. In this paper, we pr…

Critical elements in algebras of numerical events
Dietmar Dorninger, Helmut L\"anger
https://arxiv.org/abs/2507.00194 https://ar…

Critical elements in algebras of numerical events
The probability p(s) of the occurrence of an event pertaining to a physical system which is observed in different states s determines a function p from the set S of states of the system to [0,1]. The function p is called a numerical event or more precisely an S-probability. When appropriately structured, sets P of numerical events form so-called algebras of S-probabilities, which are orthomodular posets that can serve as quantum logics. If one deals with a classical physical system, then P will…

This https://arxiv.org/abs/2502.19311 has been replaced.
initial toot: https://mastoxiv.page/@arXiv_csLO_…

Faithful Logic Embeddings in HOL -- Deep and Shallow
Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embedd…

Solving MDPs with LTLf and PPLTL Temporal Objectives
Giuseppe De Giacomo, Yong Li, Sven Schewe, Christoph Weinhuber, Pian Yu
https://arxiv.org/abs/2505.17264

Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives
The temporal logics LTLf+ and PPLTL+ have recently been proposed to express objectives over infinite traces. These logics are appealing because they match the expressive power of LTL on infinite traces while enabling efficient DFA-based techniques, which have been crucial to the scalability of reactive synthesis and adversarial planning in LTLf and PPLTL over finite traces. In this paper, we demonstrate that these logics are also highly effective in the context of MDPs. Introducing a technique …

Recursive Difference Categories and Topos-Theoretic Universality
Andreu Ballus Santacana
https://arxiv.org/abs/2505.22931 https://arx…

Recursive Difference Categories and Topos-Theoretic Universality
We introduce a radically minimal categorical foundation for logic, semantics, and computation, built from a single generative axiom of recursive difference. From the null mnema M0 and iterated labeled extensions by D, we form the free category M and its sheaf topos Sh(M). We prove: Modal completeness: Lawvere-Tierney topologies on Sh(M) classify all standard modal logics (K, T, S4, S5) purely via submonoids of the free monoid D*. Fixed-point expressivity: The internal mu-calculus over infin…

Model-theoretic Forcing in Transition Algebra
Go Hashimoto, Daniel G\u{a}in\u{a}
https://arxiv.org/abs/2506.22828 https://arxiv.org/p…

Model-theoretic Forcing in Transition Algebra
We study Löwenheim-Skolem and Omitting Types theorems in Transition Algebra, a logical system obtained by enhancing many sorted first-order logic with features from dynamic logic. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to actions in dynamic logics to define necessity and possibility operators. We show that Upward Löwenheim-Skolem theorem, any form of compactness, and joint Robinson consistency proper…

Diamonds and Dominoes: Impossibility Results for Associative Modal Logics
S{\o}ren Brinck Knudstorp
https://arxiv.org/abs/2506.16366 https://

Diamonds and Dominoes: Impossibility Results for Associative Modal Logics
We show that for any class of Boolean algebras with an associative operator, if it contains the complex algebra of (P(N), U), its equational theory is undecidable. Equivalently, any associative normal modal logic valid over the frame (P(N), U) is undecidable. This settles a long-open question on the decidability of hyperboolean modal logic (Goranko and Vakarelov, 1999), and addresses several related problems.

Translation of Enterprise Architecture Concept to Facilitate Digital Transformation Initiatives in Vietnam: Processes, Mechanisms and Impacts
Duong Dang, Quang Bui
https://arxiv.org/abs/2505.20247

Locality in Many-Valued Structures
James Carr
https://arxiv.org/abs/2506.16206 https://arxiv.org/pdf/2506.16206

Locality in Many-Valued Structures
Many-valued models generalise the structures from classical model theory by defining truth values for a model with an arbitrary algebra. Just as algebraic varieties provide semantics for many non-classical propositional logics, models defined over algebras in a variety provide the semantics for the corresponding non-classical predicate logics. In particular models defined over varieties of residuated lattices represent the model theory for first-order substructrual logics. In this paper we st…

Aperiodic-sampled neural network controllers with closed-loop stability verifications (extended version)
Renjie Ma, Zhijian Hu, Rongni Yang, Ligang Wu
https://arxiv.org/abs/2506.18386

Aperiodic-sampled neural network controllers with closed-loop stability verifications (extended version)
In this paper, we synthesize two aperiodic-sampled deep neural network (DNN) control schemes, based on the closed-loop tracking stability guarantees. By means of the integral quadratic constraint coping with the input-output behaviour of system uncertainties/nonlinearities and the convex relaxations of nonlinear DNN activations leveraging their local sector-bounded attributes, we establish conditions to design the event- and self-triggered logics and to compute the ellipsoidal inner approximati…

Agent Interpolation for Knowledge
Marta B\'ilkov\'a, Wesley Fussner, Roman Kuznets
https://arxiv.org/abs/2505.23401 https://a…

Agent Interpolation for Knowledge
We define a new type of proof formalism for multi-agent modal logics with S5-type modalities. This novel formalism combines the features of hypersequents to represent S5 modalities with nested sequents to represent the T-like modality alternations. We show that the calculus is sound and complete, cut-free, and terminating and yields decidability and the finite model property for multi-agent S5. We also use it to prove the Lyndon (and hence Craig) interpolation property for multi-agent S5, consi…

On pre-local tabularity above $\mathrm{S4}\times \mathrm{S4}$
Ilya B. Shapirovsky, Vladislav V. Sliusarev
https://arxiv.org/abs/2506.20874 https://

On pre-local tabularity above $\mathrm{S4}\times \mathrm{S4}$
We investigate pre-local tabularity in normal extensions of the logic $\mathrm{S4}\times \mathrm{S4}$. We show that there are exactly four pre-locally tabular logics in normal extensions of products of finite height, and that every non-locally tabular logic in this family is contained in one of them. We also give an axiomatic criterion of local tabularity above the logic of products with Noetherian skeletons. Then we construct examples of pre-locally tabular extensions of $\mathrm{S4}\times \ma…

A uniform cut-elimination theorem for linear logics with fixed points and super exponentials
Esa\"ie Bauer, Alexis Saurin
https://arxiv.org/abs/2506.14327

A uniform cut-elimination theorem for linear logics with fixed points and super exponentials
In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proof of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variet…

The complexity of deciding characteristic formulae modulo nested simulation
Luca Aceto, Antonis Achilleos, Aggeliki Chalki, Anna Ingolfsdottir
https://arxiv.org/abs/2505.22277

The complexity of deciding characteristic formulae modulo nested simulation
This paper studies the complexity of determining whether a formula in the modal logics characterizing the nested-simulation semantics is characteristic for some process, which is equivalent to determining whether the formula is satisfiable and prime. The main results are that the problem of determining whether a formula is prime in the modal logic characterizing the 2-nested-simulation preorder is CoNP-complete and is PSPACE-complete in the case of the n-nested-simulation preorder, when n>= 3. …

This https://arxiv.org/abs/2505.12899 has been replaced.
initial toot: https://mastoxiv.page/@arXiv_csLO_…

Interpolation for the two-way modal mu-calculus
The two-way modal mu-calculus is the extension of the (standard) one-way mu-calculus with converse (backward-looking) modalities. For this logic we introduce two new sequent-style proof calculi: a non-wellfounded system admitting infinite branches and a finitary, cyclic version of this that employs annotations. As is common in sequent systems for two-way modal logics, our calculi feature an analytic cut rule. What distinguishes our approach is the use of so-called trace atoms, which serve to ap…

This https://arxiv.org/abs/2502.19311 has been replaced.
initial toot: https://mastoxiv.page/@arXiv_csLO_…

Faithful Logic Embeddings in HOL -- Deep and Shallow
Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embedd…

Swap Kripke models for deontic LFIs
Mahan Vaz, Marcelo E. Coniglio
https://arxiv.org/abs/2506.06181 https://arxiv.org/pdf/2506.06181

Swap Kripke models for deontic LFIs
We present a construction of nondeterministic semantics for some deontic logics based on the class of paraconsistent logics known as Logics of Formal Inconsistency (LFIs), for the first time combining swap structures and Kripke models through the novel notion of swap Kripe models. We start by making use of Nmatrices to characterize systems based on LFIs that do not satisfy axiom (cl), while turning to RNmatrices when the latter is considered in the underlying LFIs. This paper also presents, for…

Homomorphism Indistinguishability and Game Comonads for Restricted Conjunction and Requantification
Georg Schindling
https://arxiv.org/abs/2506.19746 https…

Homomorphism Indistinguishability and Game Comonads for Restricted Conjunction and Requantification
The notion of homomorphism indistinguishability offers a combinatorial framework for characterizing equivalence relations of graphs, in particular equivalences in counting logics within finite model theory. That is, for certain graph classes, two structures agree on all homomorphism counts from the class if and only if they satisfy the same sentences in a corresponding logic. This perspective often reveals connections between the combinatorial properties of graph classes and the syntactic struc…

Proceedings of the 19th International Workshop on Logical and Semantic Frameworks, with Applications
Cynthia Kop (Radboud Universiteit Nijmegen), Helida Salles Santos (Universidade Federal do Rio Grande)
https://arxiv.org/abs/2506.05219

Proceedings of the 19th International Workshop on Logical and Semantic Frameworks, with Applications
This volume contains the post-proceedings of the 19th LSFA, which was held in Goiânia, the capital of Goiás state in Brazil, from September 18 to September 20, 2024. Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and programming languages, supporting tool development and reasoning. The aim of this series is bringing together theoreticians and practitioners t…