Logic in Computer Science

Authors and titles for January 2024

[1] arXiv:2401.00164 [pdf, html, other]

Title: Solving Causal Stream Inclusions

Harald Ruess

Subjects: Logic in Computer Science (cs.LO)

[2] arXiv:2401.00512 [pdf, other]

Title: A parametricity-based formalization of semi-simplicial and semi-cubical sets

Hugo Herbelin, Ramkumar Ramachandra

Comments: Version corresponds to the published version (though with a different formatting). Associated formalization in Coq at this https URL

Journal-ref: Math. Struct. Comp. Sci. 35 (2025) e13

Subjects: Logic in Computer Science (cs.LO)

[3] arXiv:2401.01884 [pdf, html, other]

Title: A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets

Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, Laure Petrucci

Comments: arXiv admin note: substantial text overlap with arXiv:2303.08929

Journal-ref: Fundamenta Informaticae, Volume 192, Issues 3-4: Petri Nets 2023 (November 10, 2024) fi:12781

Subjects: Logic in Computer Science (cs.LO)

[4] arXiv:2401.01893 [pdf, other]

Title: Negation and Identity in a Modal Mode Theory

Juan Afanador

Subjects: Logic in Computer Science (cs.LO)

[5] arXiv:2401.02091 [pdf, html, other]

Title: Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem

Adriano Barile, Stefano Berardi, Luca Roversi

Comments: Presented at the 24th Italian Conference on Theoretical Computer Science (ICTCS 2023), September 13-15, 2023, Palermo, Italy

Journal-ref: CEUR Workshop Proceedings, Vol-3587, Proceedings of the 24th Italian Conference on Theoretical Computer Science, Giuseppa Castiglione and Marinella Sciortino (eds.), 2023, pp. 31-43, https://ceur-ws.org/Vol-3587/

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)

[6] arXiv:2401.02239 [pdf, html, other]

Title: A Decision Method for Elementary Stream Calculus

Harald Ruess

Comments: 19 pages

Subjects: Logic in Computer Science (cs.LO)

[7] arXiv:2401.02745 [pdf, html, other]

Title: Substitution in the lambda Calculus and the role of the Curry School

Fairouz Kamareddine

Journal-ref: In Fairouz Kamareddine editor. A Century since Principia's Substitution Bedazzled Haskell Curry. In Honour of Jonathan Seldin's 80th Anniversary, College Publications 2023. ISSN-10 1848904363

Subjects: Logic in Computer Science (cs.LO)

[8] arXiv:2401.02869 [pdf, other]

Title: Practical Reasoning in DatalogMTL

Dingmin Wang, Przemysław A. Wałęga, Pan Hu, Bernardo Cuenca Grau

Comments: Under consideration in Theory and Practice of Logic Programming (TPLP). arXiv admin note: text overlap with arXiv:2208.07100

Journal-ref: Theory and Practice of Logic Programming 25 (2025) 225-255

Subjects: Logic in Computer Science (cs.LO)

[9] arXiv:2401.02950 [pdf, other]

Title: The Tactician's Web of Large-Scale Formal Knowledge

Lasse Blaauwbroek

Comments: 47 pages

Subjects: Logic in Computer Science (cs.LO); Machine Learning (cs.LG); Programming Languages (cs.PL)

[10] arXiv:2401.03711 [pdf, html, other]

Title: Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability

Nicolas Amat (LAAS, LAAS-VERTICS), Silvano Dal Zilio (LAAS-VERTICS), Didier Le Botlan (LAAS-VERTICS)

Journal-ref: Verification, Model Checking, and Abstract Interpretation. VMCAI 2024, Jan 2024, London, United Kingdom. pp.101-123

Subjects: Logic in Computer Science (cs.LO)

[11] arXiv:2401.04594 [pdf, html, other]

Title: Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects

Noam Zilberstein

Journal-ref: ACM Transactions on Programming Languages and Systems (TOPLAS), June 2025

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[12] arXiv:2401.05165 [pdf, html, other]

Title: Non-Numerical Weakly Relational Domains

Helmut Seidl, Julian Erhard, Sarah Tilscher, Michael Schwarz

Comments: 15 pages

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[13] arXiv:2401.05585 [pdf, html, other]

Title: Technical Report: Time-Bounded Resilience

Tajana Ban Kirigin, Jesse Comer, Max Kanovich, Andre Scedrov, Carolyn Talcott

Subjects: Logic in Computer Science (cs.LO)

[14] arXiv:2401.05842 [pdf, other]

Title: A Categorical Approach to DIBI Models

Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva, Fabio Zanasi

Comments: 33 pages

Subjects: Logic in Computer Science (cs.LO)

[15] arXiv:2401.05872 [pdf, html, other]

Title: Logical Predicates in Higher-Order Mathematical Operational Semantics

Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas, Henning Urbat

Comments: Extended version

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[16] arXiv:2401.06519 [pdf, html, other]

Title: Graded modal logic and counting message passing automata

Veeti Ahvonen, Damian Heiman, Antti Kuusisto

Subjects: Logic in Computer Science (cs.LO); Distributed, Parallel, and Cluster Computing (cs.DC)

[17] arXiv:2401.06574 [pdf, other]

Title: CTMCs with Imprecisely Timed Observations

Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga, Nils Jansen

Comments: Extended version (with appendix) of the paper accepted at TACAS 2024

Subjects: Logic in Computer Science (cs.LO)

[18] arXiv:2401.07055 [pdf, other]

Title: Diagrammatic Algebra of First Order Logic

Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, Pawel Sobocinski

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)

[19] arXiv:2401.07147 [pdf, other]

Title: Choiceless Computation and Symmetry: Limitations of Definability

Benedikt Pago

Comments: Appeared at CSL 2021

Journal-ref: 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 33:1-33:21, Schloss Dagstuhl - Leibniz-Zentrum f\"ur Informatik (2021)

Subjects: Logic in Computer Science (cs.LO)

[20] arXiv:2401.07548 [pdf, other]

Title: Rabin Games and Colourful Universal Trees

Rupak Majumdar, Irmak Saglam, K. S. Thejaswini

Comments: 31 pages, 4 figures. Accepted at TACAS 2024

Subjects: Logic in Computer Science (cs.LO); Data Structures and Algorithms (cs.DS); Formal Languages and Automata Theory (cs.FL)

[21] arXiv:2401.07616 [pdf, other]

Title: Model checking strategy-controlled systems in rewriting logic

Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, Alberto Verdejo

Journal-ref: Autom. Softw. Eng. 29(1) (2022) article 7

Subjects: Logic in Computer Science (cs.LO)

[22] arXiv:2401.07680 [pdf, other]

Title: Strategies, model checking and branching-time properties in Maude

Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, Alberto Verdejo

Journal-ref: J. Log. Algebraic Methods Program. 123 (2021) article 100700

Subjects: Logic in Computer Science (cs.LO)

[23] arXiv:2401.07743 [pdf, other]

Title: Simulating and model checking membrane systems using strategies in Maude

Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, Alberto Verdejo

Journal-ref: J. Logic. Algebr. Program 124 (2022) article 100727

Subjects: Logic in Computer Science (cs.LO)

[24] arXiv:2401.07749 [pdf, other]

Title: Metalevel transformation of strategies

Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, Alberto Verdejo

Journal-ref: J. Logic. Algebr. Program 124 (2022) article 100728

Subjects: Logic in Computer Science (cs.LO)

[25] arXiv:2401.07914 [pdf, other]

Title: Graphical Symplectic Algebra

Robert I. Booth, Titouan Carette, Cole Comfort

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT); Symplectic Geometry (math.SG); Quantum Physics (quant-ph)

[26] arXiv:2401.08377 [pdf, other]

Title: Pareto Curves for Compositionally Model Checking String Diagrams of MDPs

Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot, Sebastian Junges

Comments: Extended version (includes the Appendix) of the paper accepted at TACAS-24

Subjects: Logic in Computer Science (cs.LO)

[27] arXiv:2401.08445 [pdf, html, other]

Title: Algebraic Reasoning over Relational Structures

Jan Jurka, Stefan Milius, Henning Urbat

Journal-ref: Electronic Notes in Theoretical Informatics and Computer Science, Volume 4 - Proceedings of MFPS XL (December 11, 2024) entics:14598

Subjects: Logic in Computer Science (cs.LO)

[28] arXiv:2401.09270 [pdf, other]

Title: Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics

Todd Waugh Ambridge

Comments: A thesis submitted to the University of Birmingham for the degree of Doctor of Philosophy. 198 pages. Supervised by Dan Ghica and Martín Escardó

Subjects: Logic in Computer Science (cs.LO)

[29] arXiv:2401.09273 [pdf, html, other]

Title: A classification of bisimilarities for general Markov decision processes

Martín Santiago Moroni, Pedro Sánchez Terraf

Comments: 40 pages. v2: Reference to prior example due to D. Gburek and added acknowledgment. v3: We thank Referee 1 for a simplified Example 3.32, and for making us realize that the argument involving Bernstein sets was flawed; Referee 2's observations helped us to streamline the discussion at the end of Section 3.4

Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)

[30] arXiv:2401.09366 [pdf, html, other]

Title: An Introduction to Different Approaches to Initial Semantics

Thomas Lamiaux, Benedikt Ahrens

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[31] arXiv:2401.09860 [pdf, other]

Title: Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version)

Luca Geatti, Alessio Mansutti, Angelo Montanari

Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)

[32] arXiv:2401.09973 [pdf, html, other]

Title: Integrating Loop Acceleration into Bounded Model Checking

Florian Frohn, Jürgen Giesl

Subjects: Logic in Computer Science (cs.LO)

[33] arXiv:2401.10553 [pdf, other]

Title: Single-set cubical categories and their formalisation with a proof assistant (extended version)

Philippe Malbos, Tanguy Massacrier, Georg Struth

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)

[34] arXiv:2401.10638 [pdf, other]

Title: Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains

Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler

Subjects: Logic in Computer Science (cs.LO); Probability (math.PR)

[35] arXiv:2401.10703 [pdf, html, other]

Title: DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories

Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike, John Backes

Subjects: Logic in Computer Science (cs.LO)

[36] arXiv:2401.10725 [pdf, other]

Title: Proceedings 14th International Conference on Automated Deduction in Geometry

Pedro Quaresma (University of Coimbra, Portugal), Zoltán Kovács (The Private University College of Education of the Diocese of Linz, Austria)

Journal-ref: EPTCS 398, 2024

Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Computational Geometry (cs.CG); Mathematical Software (cs.MS)

[37] arXiv:2401.10778 [pdf, other]

Title: HaliVer: Deductive Verification and Scheduling Languages Join Forces

Lars B. van den Haak, Anton Wijs, Marieke Huisman, Mark van den Brand

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[38] arXiv:2401.11197 [pdf, other]

Title: Timeout Asynchronous Session Types: Safe Asynchronous Mixed-Choice For Timed Interactions

Jonah Pears, Laura Bocchi, Maurizio Murgia, Andy King

Journal-ref: Logical Methods in Computer Science, Volume 21, Issue 3 (July 23, 2025) lmcs:12913

Subjects: Logic in Computer Science (cs.LO)

[39] arXiv:2401.11266 [pdf, html, other]

Title: Lower bounds for set-blocked clauses proofs

Emre Yolcu

Comments: arXiv admin note: text overlap with arXiv:2211.12456

Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC)

[40] arXiv:2401.11290 [pdf, html, other]

Title: On Dependent Variables in Reactive Synthesis

S. Akshay, Eliyahu Basa, Supratik Chakraborty, Dror Fried

Comments: Full version of conference paper published in TACAS'24

Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)

[41] arXiv:2401.11752 [pdf, other]

Title: Univalent Enriched Categories and the Enriched Rezk Completion

Niels van der Weide

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)

[42] arXiv:2401.11861 [pdf, other]

Title: A Fixed-Parameter Study on Propositional Dynamic Logic

Mohammad Javad Hosseinpour, Farzad Didehvar

Comments: 7 pages, A version of this paper is to be submitted in the 11th annual conference of Iran Association of Logic

Subjects: Logic in Computer Science (cs.LO)

[43] arXiv:2401.11897 [pdf, other]

Title: Towards Automatic Transformations of Coq Proof Scripts

Nicolas Magaud (Lab. ICube CNRS Université de Strasbourg, France)

Comments: In Proceedings ADG 2023, arXiv:2401.10725

Journal-ref: EPTCS 398, 2024, pp. 4-10

Subjects: Logic in Computer Science (cs.LO); Symbolic Computation (cs.SC); Software Engineering (cs.SE)

[44] arXiv:2401.11904 [pdf, other]

Title: Towards an Independent Version of Tarski's System of Geometry

Pierre Boutry (Centre Inria d'Université Côte d'Azur, Sophia Antipolis, France), Stéphane Kastenbaum, Clément Saintier

Comments: In Proceedings ADG 2023, arXiv:2401.10725

Journal-ref: EPTCS 398, 2024, pp. 73-84

Subjects: Logic in Computer Science (cs.LO)

[45] arXiv:2401.12061 [pdf, other]

Title: Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL

Jonathan Julián Huerta y Munive, Simon Foster, Mario Gleirscher, Georg Struth, Christian Pardillo Laursen, Thomas Hickman

Comments: Submitted to the Journal of Automated Reasoning

Subjects: Logic in Computer Science (cs.LO); Mathematical Software (cs.MS)

[46] arXiv:2401.12067 [pdf, other]

Title: A concise proof of Commoner's theorem

Petr Jancar

Comments: A slight elaboration of the 1-page text in Petri Net Newsletter, No 49, page 43 (October 1995)

Subjects: Logic in Computer Science (cs.LO)

[47] arXiv:2401.12093 [pdf, other]

Title: Monitoring the Future of Smart Contracts

Margarita Capretto, Martin Ceresa, Cesar Sanchez

Subjects: Logic in Computer Science (cs.LO); Cryptography and Security (cs.CR)

[48] arXiv:2401.12131 [pdf, other]

Title: NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis

Matthias Cosler, Christopher Hahn, Ayham Omar, Frederik Schmitt

Subjects: Logic in Computer Science (cs.LO); Machine Learning (cs.LG)

[49] arXiv:2401.12170 [pdf, other]

Title: Natural Strategic Ability in Stochastic Multi-Agent Systems

Raphaël Berthon, Joost-Pieter Katoen, Munyque Mittelmann, Aniello Murano

Comments: Extended version of the paper accepted at AAAI 2024

Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI)

[50] arXiv:2401.12212 [pdf, other]

Title: Genericity Through Stratification

Victor Arrial, Giulio Guerrieri, Delia Kesner

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[51] arXiv:2401.12385 [pdf, other]

Title: A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations

Patrick Baillot, Ugo Dal Lago, Cynthia Kop, Deivid Vale

Comments: This version subsumes the older conference version. It is submitted (to LMCS) as an special issue paper in honour of FoSSaCs 2024

Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC)

[52] arXiv:2401.12638 [pdf, other]

Title: On The Axioms Of $\mathcal{M},\mathcal{N}$-Adhesive Categories

Davide Castelnovo, Marino Miculan

Journal-ref: Logical Methods in Computer Science, Volume 21, Issue 1 (March 6, 2025) lmcs:12930

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)

[53] arXiv:2401.12703 [pdf, other]

Title: Small Test Suites for Active Automata Learning

Loes Kruger, Sebastian Junges, Jurriaan Rot

Comments: Extended paper for TACAS 2024

Subjects: Logic in Computer Science (cs.LO)

[54] arXiv:2401.13328 [pdf, html, other]

Title: Rank-decreasing transductions

Mikołaj Bojańczyk, Pierre Ohlmann

Comments: 22 pages, 13 figures

Subjects: Logic in Computer Science (cs.LO)

[55] arXiv:2401.13369 [pdf, html, other]

Title: Dynamic Epistemic Logic of Resource Bounded Information Mining Agents

Vitaliy Dolgorukov, Rustam Galimullin, Maksim Gladyshev

Subjects: Logic in Computer Science (cs.LO)

[56] arXiv:2401.13382 [pdf, html, other]

Title: A proof theory of right-linear (omega-)grammars via cyclic proofs

Anupam Das, Abhishek De

Comments: 34 pages, 3 figures

Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL); Logic (math.LO)

[57] arXiv:2401.13390 [pdf, html, other]

Title: Memoryless Strategies in Stochastic Reachability Games

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Subjects: Logic in Computer Science (cs.LO); Computer Science and Game Theory (cs.GT); Probability (math.PR)

[58] arXiv:2401.13700 [pdf, html, other]

Title: Towards Automated Readable Proofs of Ruler and Compass Constructions

Vesna Marinković (Faculty of Mathematics, University of Belgrade), Tijana Šukilović (Faculty of Mathematics, University of Belgrade), Filip Marić (Faculty of Mathematics, University of Belgrade)

Comments: In Proceedings ADG 2023, arXiv:2401.10725

Journal-ref: EPTCS 398, 2024, pp. 11-20

Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI)

[59] arXiv:2401.14106 [pdf, html, other]

Title: Epimorphisms and Acyclic Types in Univalent Foundations

Ulrik Buchholtz, Tom de Jong, Egbert Rijke

Comments: To appear in The Journal of Symbolic Logic

Subjects: Logic in Computer Science (cs.LO); Algebraic Topology (math.AT); Category Theory (math.CT)

[60] arXiv:2401.14126 [pdf, other]

Title: An Indexed Linear Logic for Idempotent Intersection Types (Long version)

Flavien Breuvart, Federico Olimpieri

Subjects: Logic in Computer Science (cs.LO)

[61] arXiv:2401.14516 [pdf, html, other]

Title: Beyond the Spell: A Dynamic Logic Analysis of Misdirection

Benjamin Icard, Raul Fervari

Subjects: Logic in Computer Science (cs.LO)

[62] arXiv:2401.14763 [pdf, other]

Title: Comparing Session Type Systems derived from Linear Logic

Bas van den Heuvel, Jorge A. Pérez

Comments: Preprint to appear in JLAMP; revised/extended version of this https URL

Subjects: Logic in Computer Science (cs.LO)

[63] arXiv:2401.14834 [pdf, other]

Title: From Differential Linear Logic to Coherent Differentiation

Thomas Ehrhard (IRIF, Inria)

Subjects: Logic in Computer Science (cs.LO)

[64] arXiv:2401.14957 [pdf, other]

Title: Declassification Policy for Program Complexity Analysis

Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, Romain Péchoux

Subjects: Logic in Computer Science (cs.LO)

[65] arXiv:2401.14996 [pdf, html, other]

Title: A Resolution-Based Interactive Proof System for UNSAT

Philipp Czerner, Javier Esparza, Valentin Krasotin, Adrian Krauss

Comments: 26 pages

Subjects: Logic in Computer Science (cs.LO)

[66] arXiv:2401.15037 [pdf, other]

Title: On symmetries of spheres in univalent foundations

Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus, Marc Bezem

Comments: comments welcome

Subjects: Logic in Computer Science (cs.LO); Algebraic Topology (math.AT)

[67] arXiv:2401.15258 [pdf, html, other]

Title: Foundations of Substructural Dependent Type Theory

C.B. Aberlé

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL); Category Theory (math.CT)

[68] arXiv:2401.16015 [pdf, other]

Title: Querying Fault and Attack Trees: Property Specification on a Water Network

Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn, Mariëlle Stoelinga

Subjects: Logic in Computer Science (cs.LO)

[69] arXiv:2401.16109 [pdf, html, other]

Title: Minimalistic System Modelling: Behaviours, Interfaces, and Local Reasoning

Didier Galmiche, Timo Lang, David Pym

Comments: 24 pages

Subjects: Logic in Computer Science (cs.LO)

[70] arXiv:2401.16230 [pdf, html, other]

Title: Elementary first-order model checking for sparse graphs

Jakub Gajarský, Michał Pilipczuk, Marek Sokołowski, Giannos Stamoulis, Szymon Toruńczyk

Comments: 44 pages

Subjects: Logic in Computer Science (cs.LO); Discrete Mathematics (cs.DM); Data Structures and Algorithms (cs.DS); Combinatorics (math.CO); Logic (math.LO)

[71] arXiv:2401.16366 [pdf, other]

Title: Choiceless Polynomial Space

Flavio Ferrarotti, Klaus-Dieter Schewe

Comments: 12 pages. arXiv admin note: substantial text overlap with arXiv:2005.04598

Subjects: Logic in Computer Science (cs.LO)

[72] arXiv:2401.16838 [pdf, html, other]

Title: A Complete Fragment of LTL(EB)

Flavio Ferrarotti, Peter Rivière, Klaus-Dieter Schewe, Neeraj Kumar Singh, Yamine Aït Ameur

Comments: 22 pages

Subjects: Logic in Computer Science (cs.LO)

[73] arXiv:2401.16888 [pdf, html, other]

Title: The Thins Ordering on Relations

Ed Voermans, Jules Desharnais, Roland Backhouse

Comments: The open problem posed in the first-submitted version of this paper has been successfully resolved. As a consequence, the additional axiom is no longer required

Subjects: Logic in Computer Science (cs.LO)

[74] arXiv:2401.17130 [pdf, other]

Title: Diagonals and Block-Ordered Relations

Roland Backhouse, Ed Voermans

Subjects: Logic in Computer Science (cs.LO)

[75] arXiv:2401.17199 [pdf, other]

Title: A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)

Victoria Vollmer, Danielle Marshall, Harley Eades III, Dominic Orchard

Comments: Published in 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[76] arXiv:2401.17226 [pdf, html, other]

Title: Knowledge Problems in Protocol Analysis: Extending the Notion of Subterm Convergent

Carter Bunch, Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen

Comments: Preprint submitted to Logical Methods in Computer Science. Updated based on journal reviews

Subjects: Logic in Computer Science (cs.LO)

[77] arXiv:2401.17483 [pdf, html, other]

Title: An Analysis of Symmetry in Quantitative Semantics

Pierre Clairambault, Simon Forest

Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)

[78] arXiv:2401.17832 [pdf, html, other]

Title: SAT-Based Subsumption Resolution

Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath

Journal-ref: Automated Deduction -- CADE 29 (2023). Lecture Notes in Computer Science vol 14132. Springer

Subjects: Logic in Computer Science (cs.LO)

[79] arXiv:2401.00757 (cross-list from cs.SE) [pdf, html, other]

Title: LogicAsker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models

Yuxuan Wan, Wenxuan Wang, Yiliu Yang, Youliang Yuan, Jen-tse Huang, Pinjia He, Wenxiang Jiao, Michael R. Lyu

Comments: Accepted by EMNLP 2024

Subjects: Software Engineering (cs.SE); Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Logic in Computer Science (cs.LO)

[80] arXiv:2401.00963 (cross-list from cs.SE) [pdf, other]

Title: Leveraging Large Language Models to Boost Dafny's Developers Productivity

Álvaro Silva, Alexandra Mendes, João F. Ferreira

Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[81] arXiv:2401.01096 (cross-list from math.LO) [pdf, other]

Title: Demystifying $μ$

Bahareh Afshari, Graham E. Leigh, Guillermo Menèndez Turata

Subjects: Logic (math.LO); Logic in Computer Science (cs.LO)

[82] arXiv:2401.02618 (cross-list from cs.SE) [pdf, html, other]

Title: Regular Abstractions for Array Systems

Chih-Duo Hong, Anthony W. Lin

Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO)

[83] arXiv:2401.02806 (cross-list from math.HO) [pdf, html, other]

Title: The paradoxes and the infinite dazzled ancient mathematics and continue to do so today

Fairouz Kamareddine, Jonathan Seldin

Comments: To appear in 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)

Subjects: History and Overview (math.HO); Logic in Computer Science (cs.LO)

[84] arXiv:2401.02948 (cross-list from cs.PL) [pdf, other]

Title: Hashing Modulo Context-Sensitive $α$-Equivalence

Lasse Blaauwbroek, Miroslav Olšák, Herman Geuvers

Comments: 33 pages

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[85] arXiv:2401.03265 (cross-list from math.LO) [pdf, html, other]

Title: Finite Hilbert systems for Weak Kleene logics

Vitor Greati, Sérgio Marcelino, Umberto Rivieccio

Comments: Corrections on Def.2, Def.3 (PWK system) and Rem. 4

Subjects: Logic (math.LO); Logic in Computer Science (cs.LO)

[86] arXiv:2401.03274 (cross-list from math.LO) [pdf, html, other]

Title: Generating proof systems for three-valued propositional logics

Vitor Greati, Giuseppe Greco, Sérgio Marcelino, Alessandra Palmigiano, Umberto Rivieccio

Subjects: Logic (math.LO); Logic in Computer Science (cs.LO)

[87] arXiv:2401.03811 (cross-list from cs.FL) [pdf, other]

Title: The Complexity of Simplifying $ω$-Automata through the Alternating Cycle Decomposition

Antonio Casares, Corto Mascle

Comments: Full version of a paper accepted at MFCS 2024. v2: Results updated to apply to both automata with single and multiple colours per transition

Subjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)

[88] arXiv:2401.03991 (cross-list from cs.AI) [pdf, other]

Title: Advancing Spatial Reasoning in Large Language Models: An In-Depth Evaluation and Enhancement Using the StepGame Benchmark

Fangjun Li, David C. Hogg, Anthony G. Cohn

Comments: Camera-Ready version for AAAI 2024

Subjects: Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Databases (cs.DB); Logic in Computer Science (cs.LO)

[89] arXiv:2401.04068 (cross-list from eess.SY) [pdf, html, other]

Title: IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes

Frederik Baymler Mathiesen, Morteza Lahijanian, Luca Laurenti

Subjects: Systems and Control (eess.SY); Logic in Computer Science (cs.LO)

[90] arXiv:2401.04606 (cross-list from cs.DB) [pdf, html, other]

Title: The Importance of Parameters in Database Queries

Amir Gilad, Martin Grohe, Benny Kimelfeld, Peter Lindner, Christoph Standke

Subjects: Databases (cs.DB); Logic in Computer Science (cs.LO)

[91] arXiv:2401.04758 (cross-list from cs.DB) [pdf, other]

Title: On The Reasonable Effectiveness of Relational Diagrams: Explaining Relational Query Patterns and the Pattern Expressiveness of Relational Languages

Wolfgang Gatterbauer, Cody Dunne

Comments: 71 pages, 49 figures, full version of SIGMOD 2024 paper of same title: this https URL. arXiv admin note: text overlap with arXiv:2203.07284

Subjects: Databases (cs.DB); Human-Computer Interaction (cs.HC); Logic in Computer Science (cs.LO)

[92] arXiv:2401.06962 (cross-list from math.LO) [pdf, html, other]

Title: Knowability as continuity: a topological account of informational dependence

Alexandru Baltag, Johan van Benthem

Comments: 65 pages

Subjects: Logic (math.LO); Logic in Computer Science (cs.LO)

[93] arXiv:2401.07656 (cross-list from cs.AI) [pdf, other]

Title: Learning Explainable and Better Performing Representations of POMDP Strategies

Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky, Stefanie Mohr

Comments: Technical report for the submission to TACAS 24

Subjects: Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Logic in Computer Science (cs.LO)

[94] arXiv:2401.07890 (cross-list from cs.AI) [pdf, html, other]

Title: A Strategy for Implementing description Temporal Dynamic Algorithms in Dynamic Knowledge Graphs by SPIN

Alireza Shahbazi, Seyyed Ahmad Mirsanei, Malikeh Haj Khan Mirzaye Sarraf, Behrouz Minaei Bidgoli

Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

[95] arXiv:2401.07996 (cross-list from cs.FL) [pdf, other]

Title: Satisfiability of Context-free String Constraints with Subword-ordering and Transducers

C Aiswarya, Soumodev Mal, Prakash Saivasan

Subjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)

[96] arXiv:2401.08366 (cross-list from cs.CC) [pdf, html, other]

Title: On the formalization of the notion of an algorithm

C. A. Middelburg

Comments: 22 pages, revision of v1, presentation improved at several places and some minor errors corrected

Journal-ref: In The Practice of Formal Methods, pages 23--44. Springer Nature, LNCS 14781, 2024

Subjects: Computational Complexity (cs.CC); Data Structures and Algorithms (cs.DS); Logic in Computer Science (cs.LO)

[97] arXiv:2401.09053 (cross-list from math.LO) [pdf, html, other]

Title: On some computational properties of open sets

Dag Normann, Sam Sanders

Comments: 33 pages, 1 figure, to appear in Journal of Logic and Computation. Section 5 of this paper corrects a technical error in the lambda calculus from arXiv:2203.05250

Subjects: Logic (math.LO); Logic in Computer Science (cs.LO)

[98] arXiv:2401.09678 (cross-list from cs.SE) [pdf, html, other]

Title: Integrating Graceful Degradation and Recovery through Requirement-driven Adaptation

Simon Chu, Justin Koe, David Garlan, Eunsuk Kang

Comments: Pre-print for the SEAMS '24 conference (Software Engineering for Adaptive and Self-Managing Systems Conference)

Subjects: Software Engineering (cs.SE); Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO); Systems and Control (eess.SY)

[99] arXiv:2401.10036 (cross-list from cs.CR) [pdf, html, other]

Title: LOCALINTEL: Generating Organizational Threat Intelligence from Global and Local Cyber Knowledge

Shaswata Mitra, Subash Neupane, Trisha Chakraborty, Sudip Mittal, Aritran Piplai, Manas Gaur, Shahram Rahimi

Subjects: Cryptography and Security (cs.CR); Artificial Intelligence (cs.AI); Information Retrieval (cs.IR); Logic in Computer Science (cs.LO)

[100] arXiv:2401.10154 (cross-list from math.HO) [pdf, html, other]

Title: In Memory of Martin Davis

Wesley Calvert, Valentina Harizanov, Eugenio G. Omodeo, Alberto Policriti, Alexandra Shlapentokh

Subjects: History and Overview (math.HO); Logic in Computer Science (cs.LO); Logic (math.LO); Number Theory (math.NT)

[101] arXiv:2401.10579 (cross-list from quant-ph) [pdf, other]

Title: Trade-offs between classical and quantum space using spooky pebbling

Arend-Jan Quist, Alfons Laarman

Subjects: Quantum Physics (quant-ph); Logic in Computer Science (cs.LO)

[102] arXiv:2401.10781 (cross-list from cs.AI) [pdf, other]

Title: Metric Dynamic Equilibrium Logic

Arvid Becker, Pedro Cabalar, Martín Diéguez, Luis Fariñas, Torsten Schaub, Anna Schuhmann

Comments: arXiv admin note: text overlap with arXiv:2304.14778

Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

[103] arXiv:2401.10937 (cross-list from econ.TH) [pdf, html, other]

Title: Subjective Causality

Joseph Y. Halpern, Evan Piermont

Subjects: Theoretical Economics (econ.TH); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

[104] arXiv:2401.10969 (cross-list from cs.AI) [pdf, other]

Title: MacroSwarm: A Field-based Compositional Framework for Swarm Programming

Gianluca Aguzzi, Roberto Casadei, Mirko Viroli

Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Software Engineering (cs.SE)

[105] arXiv:2401.11364 (cross-list from cs.CR) [pdf, html, other]

Title: Folding Custom Gates with Verifier Input

Aard Vark, Yan X Zhang

Subjects: Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO)

[106] arXiv:2401.11627 (cross-list from cs.LG) [pdf, html, other]

Title: Tight Verification of Probabilistic Robustness in Bayesian Neural Networks

Ben Batten, Mehran Hosseini, Alessio Lomuscio

Comments: Accepted at AISTATS 2024

Subjects: Machine Learning (cs.LG); Artificial Intelligence (cs.AI); Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)

[107] arXiv:2401.11807 (cross-list from math.LO) [pdf, html, other]

Title: The weakness of finding descending sequences in ill-founded linear orders

Jun Le Goh, Arno Pauly, Manlio Valenti

Comments: This is an extended version of the homonymous paper published in: Twenty Years of Theoretical and Practical Synergies. CiE 2024. Lecture Notes in Computer Science, vol 14773, pp. 339-350

Subjects: Logic (math.LO); Logic in Computer Science (cs.LO); Combinatorics (math.CO)

[108] arXiv:2401.11898 (cross-list from cs.AI) [pdf, other]

Title: Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving

Salwa Tabet Gonzalez (University of Strasbourg), Predrag Janičić (University of Belgrade), Julien Narboux (University of Strasbourg)

Comments: In Proceedings ADG 2023, arXiv:2401.10725

Journal-ref: EPTCS 398, 2024, pp. 21-37

Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

[109] arXiv:2401.11905 (cross-list from cs.AI) [pdf, other]

Title: Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry

Pedro Quaresma (University of Coimbra), Pierluigi Graziani (University of Urbino), Stefano M. Nicoletti (University of Twente)

Comments: In Proceedings ADG 2023, arXiv:2401.10725

Journal-ref: EPTCS 398, 2024, pp. 85-100

Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

[110] arXiv:2401.12113 (cross-list from cs.LG) [pdf, html, other]

Title: Extracting Formulae in Many-Valued Logic from Deep Neural Networks

Yani Zhang, Helmut Bölcskei

Comments: Signicant extension of the previous version

Subjects: Machine Learning (cs.LG); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

[111] arXiv:2401.12641 (cross-list from math.LO) [pdf, html, other]

Title: Sequential discontinuity and first-order problems

Arno Pauly, Giovanni Soldà

Subjects: Logic (math.LO); Logic in Computer Science (cs.LO); General Topology (math.GN)

[112] arXiv:2401.12731 (cross-list from cs.AI) [pdf, html, other]

Title: The Distributional Uncertainty of the SHAP score in Explainable Machine Learning

Santiago Cifuentes, Leopoldo Bertossi, Nina Pardal, Sergio Abriola, Maria Vanina Martinez, Miguel Romero

Comments: In ECAI 2024 proceedings

Subjects: Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Logic in Computer Science (cs.LO)

[113] arXiv:2401.12744 (cross-list from cs.PL) [pdf, html, other]

Title: Monadic Intersection Types, Relationally (Extended Version)

Francesco Gavazzo, Riccardo Treglia, Gabriele Vanoni

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[114] arXiv:2401.12947 (cross-list from cs.CL) [pdf, html, other]

Title: Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion

Dylan Zhang, Curt Tigges, Zory Zhang, Stella Biderman, Maxim Raginsky, Talia Ringer

Comments: arXiv admin note: text overlap with arXiv:2305.14699

Subjects: Computation and Language (cs.CL); Artificial Intelligence (cs.AI); Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[115] arXiv:2401.13597 (cross-list from math.LO) [pdf, other]

Title: Base-extension Semantics for Modal Logic

Timo Eckhardt, David J. Pym

Comments: Accepted to be published in the Logic Journal of the IGPL

Subjects: Logic (math.LO); Logic in Computer Science (cs.LO)

[116] arXiv:2401.14244 (cross-list from cs.SE) [pdf, html, other]

Title: Contract Usage and Evolution in Android Mobile Applications

David R. Ferreira, Alexandra Mendes, João F. Ferreira

Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[117] arXiv:2401.14286 (cross-list from cs.PL) [pdf, other]

Title: Equivalence of Applicative Functors and Multifunctors

Andreas Abel

Comments: 6 pages

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[118] arXiv:2401.14303 (cross-list from cs.FL) [pdf, other]

Title: On Some Complexity Results for Even Linear Languages

Liliana Cojocaru

Comments: 16 pages, no figure. arXiv admin note: substantial text overlap with arXiv:1512.09207

Subjects: Formal Languages and Automata Theory (cs.FL); Computational Complexity (cs.CC); Logic in Computer Science (cs.LO)

[119] arXiv:2401.14320 (cross-list from cs.SE) [pdf, other]

Title: Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis

Florian Lanzinger, Christian Martin, Frederik Reiche, Samuel Teuber, Robert Heinrich, Alexander Weigl

Comments: 10 pages; to appear at the 39th ACM/SIGAPP Symposium on Applied Computing (SAC '24)

Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO)

[120] arXiv:2401.14461 (cross-list from cs.AI) [pdf, html, other]

Title: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks

Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark Barrett

Comments: Condensed version accepted at CAV'24

Subjects: Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Logic in Computer Science (cs.LO)

[121] arXiv:2401.14961 (cross-list from cs.LG) [pdf, other]

Title: Set-Based Training for Neural Network Verification

Lukas Koller, Tobias Ladner, Matthias Althoff

Subjects: Machine Learning (cs.LG); Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO)

[122] arXiv:2401.15186 (cross-list from cs.CC) [pdf, other]

Title: The Rise of Plurimorphisms: Algebraic Approach to Approximation

Libor Barto, Silvia Butti, Alexandr Kazda, Caterina Viola, Stanislav Živný

Comments: A full version of a LICS 2024 paper

Subjects: Computational Complexity (cs.CC); Discrete Mathematics (cs.DM); Logic in Computer Science (cs.LO)

[123] arXiv:2401.15384 (cross-list from cs.FL) [pdf, other]

Title: Positional $ω$-regular languages

Antonio Casares, Pierre Ohlmann

Comments: Full version of a paper accepted at LICS 2024

Subjects: Formal Languages and Automata Theory (cs.FL); Computer Science and Game Theory (cs.GT); Logic in Computer Science (cs.LO)

[124] arXiv:2401.16215 (cross-list from cs.LG) [pdf, other]

Title: Learning big logical rules by joining small rules

Céline Hocquette, Andreas Niskanen, Rolf Morel, Matti Järvisalo, Andrew Cropper

Subjects: Machine Learning (cs.LG); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

[125] arXiv:2401.16336 (cross-list from math.AT) [pdf, html, other]

Title: Computational Synthetic Cohomology Theory in Homotopy Type Theory

Axel Ljungström, Anders Mörtberg

Comments: v2: minor typos, updated acknowledgements

Journal-ref: Math. Struct. Comp. Sci. 35 (2025) e16

Subjects: Algebraic Topology (math.AT); Logic in Computer Science (cs.LO)

[126] arXiv:2401.16383 (cross-list from cs.LG) [pdf, other]

Title: Learning logic programs by finding minimal unsatisfiable subprograms

Andrew Cropper, Céline Hocquette

Subjects: Machine Learning (cs.LG); Logic in Computer Science (cs.LO)

[127] arXiv:2401.16998 (cross-list from cs.DS) [pdf, other]

Title: The Sherali-Adams and Weisfeiler-Leman hierarchies in (Promise Valued) Constraint Satisfaction Problems

Libor Barto, Silvia Butti, Víctor Dalmau

Comments: A joint extended version of arXiv:2107.02956 and arXiv:2205.04805

Subjects: Data Structures and Algorithms (cs.DS); Logic in Computer Science (cs.LO)

[128] arXiv:2401.17159 (cross-list from cs.AI) [pdf, html, other]

Title: Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis

Zhengyang Lu, Stefan Siemer, Piyush Jha, Joel Day, Florin Manea, Vijay Ganesh

Comments: Accepted at IJCAI 2024

Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Software Engineering (cs.SE)

[129] arXiv:2401.17169 (cross-list from cs.CL) [pdf, html, other]

Title: Conditional and Modal Reasoning in Large Language Models

Wesley H. Holliday, Matthew Mandelkern, Cedegao E. Zhang

Comments: Accepted for The 2024 Conference on Empirical Methods in Natural Language Processing (EMNLP 2024). Final version includes additional models and additional inference patterns

Subjects: Computation and Language (cs.CL); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)

[130] arXiv:2401.17444 (cross-list from cs.FL) [pdf, html, other]

Title: Higher-Dimensional Timed Automata for Real-Time Concurrency

Amazigh Amrane, Hugo Bazille, Emily Clement, Uli Fahrenberg, Philipp Schlehuber-Caissier

Subjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)

[131] arXiv:2401.18029 (cross-list from cs.PL) [pdf, other]

Title: Context-Sensitive Abstract Interpretation of Dynamic Languages

Franciszek Piszcz

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO); Software Engineering (cs.SE)