Logic in Computer Science

Authors and titles for December 2024

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

Title: Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification

Conrad Zimmerman, Jenna DiVincenzo

Comments: For presentation at the 1st Workshop on the Theory and Practice of Static Analysis (TPSA 2025)

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

[2] arXiv:2412.00356 [pdf, html, other]

Title: Vagueness and the Connectives

Wesley H. Holliday

Comments: Forthcoming in The Connectives in Logic and Language, eds. Jialiang Yan, Mingming Liu, Dag Westerståhl, and Xiaolu Yang, Lecture Notes in Computer Science, Vol. 15410, Springer, 2025

Subjects: Logic in Computer Science (cs.LO)

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

Title: Towards a Proof System for Probabilistic Dynamic Logic

Einar Broch Johnsen, Eduard Kamburjan, Raúl Pardo, Erik Voogd, Andrzej Wąsowski

Comments: Pre-print of paper appearing in "In Principles of Verification: Cycling the Probabilistic Landscape-Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, 2024" (this https URL)

Subjects: Logic in Computer Science (cs.LO)

[4] arXiv:2412.01484 [pdf, html, other]

Title: Definite Descriptions and Hybrid Tense Logic

Andrzej Indrzejczak, Michał Zawidzki

Journal-ref: Synthese 202, 98 (2023)

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

[5] arXiv:2412.01667 [pdf, other]

Title: Generating Higher Identity Proofs in Homotopy Type Theory

Thibaut Benjamin

Comments: 29 pages

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

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

Title: Uniform Cut-free Bisequent Calculi for Three-valued Logics

Andrzej Indrzejczak, Yaroslav Petrukhin

Journal-ref: Logic and Logical Philosophy. Vol. 33, no. 3, pp. 463--506. 2024

Subjects: Logic in Computer Science (cs.LO)

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

Title: Bisequent Calculi for Neutral Free Logic with Definite Descriptions

Andrzej Indrzejczak, Yaroslav Petrukhin

Subjects: Logic in Computer Science (cs.LO)

[8] arXiv:2412.01722 [pdf, html, other]

Title: Correspondence and Inverse Correspondence for Input/Output Logic and Region-Based Theories of Space

Andrea De Domenico, Ali Farjami, Krishna Manoorkar, Alessandra Palmigiano, Mattia Panettiere, Xiaolong Wang

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

[9] arXiv:2412.01832 [pdf, other]

Title: Targeting Completeness: Automated Complexity Analysis of Integer Programs

Nils Lommen, Éléanore Meyer, Jürgen Giesl

Comments: Journal version of IJCAR'22 (arXiv:2205.08869) and FroCoS'23 (arXiv:2307.06921) papers

Subjects: Logic in Computer Science (cs.LO)

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

Title: A Cut-free, Sound and Complete Russellian Theory of Definite Descriptions

Andrzej Indrzejczak, Nils Kürbis

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

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

Title: On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic

Tim S. Lyon

Comments: Accepted to Fundamentals of Software Engineering (FSEN) 2025

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

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

Title: CMSO-transducing tree-like graph decompositions

Rutger Campbell, Bruno Guillon, Mamadou Moustapha Kanté, Eun Jung Kim, Noleen Köhler

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

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

Title: Small Term Reachability and Related Problems for Terminating Term Rewriting Systems

Franz Baader, Jürgen Giesl

Subjects: Logic in Computer Science (cs.LO)

[14] arXiv:2412.06117 [pdf, html, other]

Title: A Logic for Paraconsistent Belief Revision based on Epistemic Entrenchment

Marcelo E. Coniglio, Martin Figallo, Rafael R. Testa

Subjects: Logic in Computer Science (cs.LO)

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

Title: Normal Nested Answer Set Programs: Syntactics, Semantics and Logical Calculi

Gonzalo E. Imaz

Subjects: Logic in Computer Science (cs.LO)

[16] arXiv:2412.06431 [pdf, other]

Title: A Program Instrumentation Framework for Automatic Verification

Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer, Marten Voorberg

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

Subjects: Logic in Computer Science (cs.LO)

[17] arXiv:2412.06509 [pdf, other]

Title: Reasoning about Strategic Abilities in Stochastic Multi-agent Systems

Yedi Zhang, Fu Song, Taolue Chen, Xuzhi Wu

Comments: Correction required and the replacement version not available shortly

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

[18] arXiv:2412.06754 [pdf, other]

Title: Probability and Angelic Nondeterminism with Multiset Semantics

Shawn Ong, Stephanie Ma, Dexter Kozen

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

[19] arXiv:2412.07341 [pdf, html, other]

Title: The Complexity of HyperQPTL

Gaëtan Regaud, Martin Zimmermann

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

Subjects: Logic in Computer Science (cs.LO)

[20] arXiv:2412.07351 [pdf, other]

Title: An Abstract Account of Up-to Techniques for Inductive Behavioural Relations

Davide Sangiorgi (OLAS, DISI)

Journal-ref: 12th International Symposium Leveraging Applications of Formal Methods Verification and Validation, ISoLA 2024, REoCAS Colloquium in Honor of Rocco De Nicola, Oct 2024, Crete Island, Greece. pp.62-74

Subjects: Logic in Computer Science (cs.LO)

[21] arXiv:2412.07986 [pdf, html, other]

Title: Provenance Analysis and Semiring Semantics for First-Order Logic

Erich Grädel, Val Tannen

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

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

[22] arXiv:2412.08234 [pdf, other]

Title: Safe Composition of Systems of Communicating Finite State Machines

Franco Barbanera (DMI - University of Catania), Rolf Hennicker (Institute for Informatics - LMU Munich)

Comments: In Proceedings ICE 2024, arXiv:2412.07570

Journal-ref: EPTCS 414, 2024, pp. 39-57

Subjects: Logic in Computer Science (cs.LO)

[23] arXiv:2412.08362 [pdf, other]

Title: Intrinsically Correct Sorting in Cubical Agda

Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide

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

[24] arXiv:2412.08624 [pdf, html, other]

Title: Efficient and Verified Continuous Double Auctions

Mohit Garg, Suneel Sarswat

Comments: 16 pages, appeared in LPAR Complementary Volume 2024

Subjects: Logic in Computer Science (cs.LO); Trading and Market Microstructure (q-fin.TR)

[25] arXiv:2412.08739 [pdf, html, other]

Title: VEL: A Formally Verified Reasoner for OWL2 EL Profile

Atalay Mert Ileri, Nalen Rangarajan, Jack Cannell, Hande McGinty

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