Logic in Computer Science

Authors and titles for April 2020

[1] arXiv:2004.00124 [pdf, other]

Title: Axiomatizing Hybrid XPath with Data

Carlos Areces, Raul Fervari

Journal-ref: Logical Methods in Computer Science, Volume 17, Issue 3 (July 20, 2021) lmcs:6259

Subjects: Logic in Computer Science (cs.LO)

[2] arXiv:2004.01320 [pdf, other]

Title: Session Type Systems based on Linear Logic: Classical versus Intuitionistic

Bas van den Heuvel (University of Groningen), Jorge A. Pérez (University of Groningen)

Comments: In Proceedings PLACES 2020, arXiv:2004.01062

Journal-ref: EPTCS 314, 2020, pp. 1-11

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

[3] arXiv:2004.01410 [pdf, other]

Title: Omission-based Abstraction for Answer Set Programs

Zeynep G. Saribatur, Thomas Eiter

Comments: Under consideration in Theory and Practice of Logic Programming (TPLP)

Journal-ref: Theory and Practice of Logic Programming 21 (2021) 145-195

Subjects: Logic in Computer Science (cs.LO)

[4] arXiv:2004.01709 [pdf, other]

Title: Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory

Bassel Mannaa, Rasmus Ejlers Møgelberg, Niccolò Veltri

Comments: 31 pages. Second version is a minor revision. arXiv admin note: text overlap with arXiv:1804.06687

Journal-ref: Logical Methods in Computer Science, Volume 16, Issue 4 (December 15, 2020) lmcs:6278

Subjects: Logic in Computer Science (cs.LO)

[5] arXiv:2004.01859 [pdf, other]

Title: Monitoring Constraints and Metaconstraints with Temporal Logics on Finite Traces

Giuseppe De Giacomo, Riccardo De Masellis, Fabrizio Maria Maggi, Marco Montali

Subjects: Logic in Computer Science (cs.LO)

[6] arXiv:2004.02120 [pdf, other]

Title: Simpler completeness proofs for modal logics with intersection

Yì N. Wáng, Thomas Ågotnes

Comments: 16 pages

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

[7] arXiv:2004.02282 [pdf, other]

Title: Clique-Width of Point Configurations

Onur Çağırıcı, Petr Hliněný, Filip Pokrývka, Abhisekh Sankaran

Subjects: Logic in Computer Science (cs.LO); Computational Geometry (cs.CG)

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

Title: The Mathematical Syntax of Architectures

Christoph F. Strnadl

Comments: 33 pages, 5 figures, 1 table, 20 definitions, 3 theorems, 1 lemma, 3 corollaries. This is a considerably extended version of v2 with new material especially concerning modularization of architectures and the new "no go" theorem

Subjects: Logic in Computer Science (cs.LO); Information Theory (cs.IT)

[9] arXiv:2004.03924 [pdf, other]

Title: Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere

Carol Mak, C.-H. Luke Ong, Hugo Paquet, Dominik Wagner

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

[10] arXiv:2004.04214 [pdf, other]

Title: Optimal Runtime Verification of Finite State Properties over Lossy Event Streams

Peeyush Kushwaha, Rahul Purandare, Matthew B. Dwyer

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

[11] arXiv:2004.04854 [pdf, other]

Title: Politeness for the Theory of Algebraic Datatypes

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett

Subjects: Logic in Computer Science (cs.LO)

[12] arXiv:2004.05287 [pdf, other]

Title: The ZX&-calculus: A complete graphical calculus for classical circuits using spiders

Cole Comfort (University of Oxford)

Comments: In Proceedings QPL 2020, arXiv:2109.01534

Journal-ref: EPTCS 340, 2021, pp. 60-90

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

[13] arXiv:2004.05392 [pdf, other]

Title: Computing with Continuous Objects: A Uniform Co-inductive Approach

Dieter Spreen

Comments: 46 pages

Journal-ref: Math. Struct. Comp. Sci. 31 (2021) 144-192

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

[14] arXiv:2004.05400 [pdf, other]

Title: Steps and Traces

Jurriaan Rot, Bart Jacobs, Paul Levy

Subjects: Logic in Computer Science (cs.LO)

[15] arXiv:2004.05688 [pdf, other]

Title: The Topological and Logical Structure of Concurrency and Dependency via Distributive Lattices

Gershom Bazerman, Raymond Puzio

Comments: 22 pages

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

[16] arXiv:2004.05802 [pdf, other]

Title: To Be Announced

Hans van Ditmarsch

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

[17] arXiv:2004.05853 [pdf, other]

Title: Generation Of A Complete Set Of Properties

Eugene Goldberg

Subjects: Logic in Computer Science (cs.LO)

[18] arXiv:2004.05943 [pdf, other]

Title: Congruence Preservation, Lattices and Recognizability

Patrick Cegielski, Serge Grigorieff, Irene Guessarian

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

[19] arXiv:2004.06637 [pdf, other]

Title: Reduction Methods on Probabilistic Control-flow Programs for Reliability Analysis

Clemens Dubslaff, Andrey Morozov, Christel Baier, Klaus Janschek

Comments: This paper is a preprint of the corresponding ESREL/PSAM 2020 conference publication

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

[20] arXiv:2004.06997 [pdf, other]

Title: Prolog Technology Reinforcement Learning Prover

Zsolt Zombori, Josef Urban, Chad E. Brown

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

[21] arXiv:2004.07058 [pdf, other]

Title: Computing Tropical Prevarieties with Satisfiability Modulo Theories (SMT) Solvers

Christoph Lüders

Subjects: Logic in Computer Science (cs.LO); Computational Geometry (cs.CG)

[22] arXiv:2004.07221 [pdf, other]

Title: First-Order Rewritability of Ontology-Mediated Queries in Linear Temporal Logic

Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev

Subjects: Logic in Computer Science (cs.LO)

[23] arXiv:2004.07390 [pdf, other]

Title: Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory

Dominik Kirst, Dominique Larchey-Wendling

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

[24] arXiv:2004.07506 [pdf, other]

Title: On Reductions of Hintikka Sets for Higher-Order Logic

Alexander Steen, Christoph Benzmüller

Comments: 10 pages; improved version

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

[25] arXiv:2004.07578 [pdf, other]

Title: Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard

Mnacho Echenim, Radu Iosif, Nicolas Peltier

Subjects: Logic in Computer Science (cs.LO)

[26] arXiv:2004.07904 [pdf, other]

Title: About the unification types of the modal logics determined by classes of deterministic frames

Philippe Balbiani, Çiğdem Gencer, Maryam Rostamigiv, Tinko Tinchev

Subjects: Logic in Computer Science (cs.LO)

[27] arXiv:2004.07940 [pdf, other]

Title: Solving bitvectors with MCSAT: explanations from bits and pieces (long version)

Stéphane Graham-Lengrand, Dejan Jovanović, Bruno Dutertre

Comments: 24 pages, long version of IJCAR'2020 conference paper

Subjects: Logic in Computer Science (cs.LO)

[28] arXiv:2004.08059 [pdf, other]

Title: A Probabilistic Logic for Verifying Continuous-time Markov Chains

Ji Guan, Nengkun Yu

Subjects: Logic in Computer Science (cs.LO)

[29] arXiv:2004.08144 [pdf, other]

Title: Intention as Commitment toward Time

Marc van Zee, Dragan Doder, Leendert van der Torre, Mehdi Dastani, Thomas Icard, Eric Pacuit

Comments: 83 pages, 4 figures, Artificial Intelligence journal pre-print

Journal-ref: Artificial Intelligence, Volume 283, June 2020, 103270

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

[30] arXiv:2004.08212 [pdf, other]

Title: Stateful Premise Selection by Recurrent Neural Networks

Bartosz Piotrowski, Josef Urban

Comments: 13 pages, 1 figure

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

[31] arXiv:2004.08213 [pdf, other]

Title: Translating Workflow Nets to Process Trees: An Algorithmic Approach

Sebastiaan J. van Zelst

Subjects: Logic in Computer Science (cs.LO)

[32] arXiv:2004.08311 [pdf, other]

Title: Finding Small Proofs for Description Logic Entailments: Theory and Practice (Extended Technical Report)

Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, Alisa Kovtunova

Comments: Extended version of a paper accepted at LPAR23

Journal-ref: LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol 73, 2020, pages 32--67

Subjects: Logic in Computer Science (cs.LO)

[33] arXiv:2004.08380 [pdf, other]

Title: Completeness of Nominal PROPs

Samuel Balco, Alexander Kurz

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

Journal-ref: Logical Methods in Computer Science, Volume 19, Issue 1 (January 26, 2023) lmcs:6313

Subjects: Logic in Computer Science (cs.LO)

[34] arXiv:2004.08440 [pdf, other]

Title: Parallelization Techniques for Verifying Neural Networks

Haoze Wu, Alex Ozdemir, Aleksandar Zeljić, Ahmed Irfan, Kyle Julian, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, Clark Barrett

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

[35] arXiv:2004.09171 [pdf, other]

Title: Reachability and liveness in parametric timed automata

Étienne André, Didier Lime, Olivier H. Roux

Comments: This manuscript is an extended version of two conference papers published in the proceedings of ICFEM 2016 and ACSD 2017

Journal-ref: Logical Methods in Computer Science, Volume 18, Issue 1 (February 9, 2022) lmcs:6312

Subjects: Logic in Computer Science (cs.LO)

[36] arXiv:2004.09450 [pdf, other]

Title: Admissibly Represented Spaces and Qcb-Spaces

Matthias Schröder

Subjects: Logic in Computer Science (cs.LO)

[37] arXiv:2004.09503 [pdf, other]

Title: On Verifying Designs With Incomplete Specification

Eugene Goldberg

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

Subjects: Logic in Computer Science (cs.LO)

[38] arXiv:2004.09621 [pdf, other]

Title: Characterizing consensus in the Heard-Of model

A.R. Balasubramanian, Igor Walukiewicz

Subjects: Logic in Computer Science (cs.LO)

[39] arXiv:2004.09777 [pdf, other]

Title: Betweenness of partial orders

Bruno Courcelle (LaBRI)

Subjects: Logic in Computer Science (cs.LO)

[40] arXiv:2004.10127 [pdf, other]

Title: Axiomatization of betweenness in order-theoretic trees

Bruno Courcelle

Journal-ref: Logical Methods in Computer Science, Volume 17, Issue 1 (February 3, 2021) lmcs:6317

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

[41] arXiv:2004.10263 [pdf, other]

Title: The Imandra Automated Reasoning System (system description)

Grant Olney Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, Nicola Mometto

Comments: To appear in Proceedings of The International Joint Conference on Automated Reasoning (IJCAR) 2020, Lecture Notes in Artificial Intelligence, Springer-Verlag

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

[42] arXiv:2004.10413 [pdf, other]

Title: Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems

Jesko Hecking-Harbusch, Niklas O. Metzger

Journal-ref: Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), Springer LNCS 11781, pages 369-386, 2019

Subjects: Logic in Computer Science (cs.LO)

[43] arXiv:2004.10654 [pdf, other]

Title: Hidden variables simulating quantum contextuality increasingly violate the Holevo bound

Adán Cabello, Joost J. Joosten

Journal-ref: In Unconventional Computing, Springer LNCS 6714 (64-76), ISSN 0302-9743. Proceedings of the 10th International Conference UC 2011, Turku, Finland 2011

Subjects: Logic in Computer Science (cs.LO)

[44] arXiv:2004.10655 [pdf, other]

Title: Formal Verification of Flow Equivalence in Desynchronized Designs

Jennifer Paykin, Brian Huffman, Daniel M. Zimmerman, Peter A. Beerel

Comments: To appear in ASYNC 2020

Subjects: Logic in Computer Science (cs.LO)

[45] arXiv:2004.10659 [pdf, other]

Title: Exponentially Huge Natural Deduction proofs are Redundant: Preliminary results on $M_\supset$

Edward Hermann Haeusler

Comments: This version has a simpler proof of the main result than the previous. Moreover, we decided to focus only on the use of this result to compress Natural Deduction huge proofs. Any relationship with computational complexity is discussed in an article that will appear in a logic journal

Subjects: Logic in Computer Science (cs.LO)

[46] arXiv:2004.10667 [pdf, other]

Title: Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)

Yutaka Nagashima

Comments: This is the preprint of our short paper accepted at the 13th Conference on Intelligent Computer Mathematics (CICM 2020)

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

[47] arXiv:2004.11185 [pdf, other]

Title: Proof Theory of Riesz Spaces and Modal Riesz Spaces

Christophe Lucas, Matteo Mio

Journal-ref: Logical Methods in Computer Science, Volume 18, Issue 1 (February 17, 2022) lmcs:6428

Subjects: Logic in Computer Science (cs.LO)

[48] arXiv:2004.11282 [pdf, other]

Title: On the proof complexity of logics of bounded branching

Emil Jeřábek

Comments: 60 pages

Journal-ref: Annals of Pure and Applied Logic 174 (2023), no. 1, article no. 103181

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

[49] arXiv:2004.11441 [pdf, other]

Title: On Skolem-hardness and saturation points in Markov decision processes

Jakob Piribauer, Christel Baier

Comments: Conference version accepted for publication at ICALP'20

Subjects: Logic in Computer Science (cs.LO)

[50] arXiv:2004.11661 [pdf, other]

Title: Invariants for Continuous Linear Dynamical Systems

Shaull Almagor, Edon Kelmendi, Joël Ouaknine, James Worrell

Comments: Full version of a ICALP 2020 paper

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

[51] arXiv:2004.11792 [pdf, other]

Title: Conditional Bisimilarity for Reactive Systems

Mathias Hülsbusch, Barbara König, Sebastian Küpper, Lara Stoltenow

Journal-ref: Logical Methods in Computer Science, Volume 18, Issue 1 (January 12, 2022) lmcs:6937

Subjects: Logic in Computer Science (cs.LO)

[52] arXiv:2004.12171 [pdf, other]

Title: Algebraic Approach to Directed Rough Sets

Mani A, Sandor Radeleczki

Comments: 37 pages, Forthcoming

Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Logic (math.LO); Rings and Algebras (math.RA)

[53] arXiv:2004.12371 [pdf, other]

Title: Monadic Decomposition in Integer Linear Arithmetic (Technical Report)

Matthew Hague, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu

Subjects: Logic in Computer Science (cs.LO)

[54] arXiv:2004.12403 [pdf, other]

Title: Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems

Ansgar Fehnker (University of Twente), Hubert Garavel (INRIA Grenoble Rhône-Alpes)

Journal-ref: EPTCS 316, 2020

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

[55] arXiv:2004.12682 [pdf, other]

Title: On the Complexity of Linear Temporal Logic with Team Semantics

Martin Lück

Subjects: Logic in Computer Science (cs.LO)

[56] arXiv:2004.12699 [pdf, other]

Title: An Efficient Floating-Point Bit-Blasting API for Verifying C Programs

Mikhail R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole

Comments: 20 pages

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

[57] arXiv:2004.12713 [pdf, other]

Title: Formal Adventures in Convex and Conical Spaces

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

Comments: to be published in CICM 2020

Subjects: Logic in Computer Science (cs.LO)

[58] arXiv:2004.12734 [pdf, other]

Title: An Epistemic Approach to the Formal Specification of Statistical Machine Learning

Yusuke Kawamoto

Comments: Accepted in Software and Systems Modeling this https URL This paper is the journal version of the SEFM'19 conference paper arXiv:1907.10327

Journal-ref: Software and Systems Modeling, Vol.20, No.2, pp.293-310, September 2020

Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Cryptography and Security (cs.CR); Machine Learning (cs.LG); Software Engineering (cs.SE)

[59] arXiv:2004.12739 [pdf, other]

Title: Dynamic complexity of Reachability: How many changes can we handle?

Samir Datta, Pankaj Kumar, Anish Mukherjee, Anuj Tawari, Nils Vortmeier, Thomas Zeume

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

[60] arXiv:2004.12740 [pdf, other]

Title: A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity

Clemens Grabmayer, Wan Fokkink

Subjects: Logic in Computer Science (cs.LO)

[61] arXiv:2004.12891 [pdf, other]

Title: The Benefit of Being Non-Lazy in Probabilistic λ-calculus

Gianluca Curzi, Michele Pagani

Subjects: Logic in Computer Science (cs.LO)

[62] arXiv:2004.12941 [pdf, other]

Title: Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs

Cameron Calk, Anupam Das, Tim Waring

Comments: 47 pages, 2 figures, 2 tables

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

[63] arXiv:2004.13287 [pdf, other]

Title: Iterative Variable Reordering: Taming Huge System Families

Clemens Dubslaff, Andrey Morozov, Christel Baier, Klaus Janschek

Comments: In Proceedings MARS 2020, arXiv:2004.12403

Journal-ref: EPTCS 316, 2020, pp. 121-133

Subjects: Logic in Computer Science (cs.LO); Performance (cs.PF); Symbolic Computation (cs.SC)

[64] arXiv:2004.13289 [pdf, other]

Title: Modeling an Asynchronous Circuit Dedicated to the Protection Against Physical Attacks

Radu Mateescu, Wendelin Serwe, Aymane Bouzafour, Marc Renaudin

Comments: In Proceedings MARS 2020, arXiv:2004.12403

Journal-ref: EPTCS 316, 2020, pp. 200-239

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

[65] arXiv:2004.13789 [pdf, other]

Title: Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes

Raphaël Berthon, Shibashis Guha, Jean-François Raskin

Comments: Paper accepted to LICS 2020 - Full version

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

[66] arXiv:2004.14195 [pdf, other]

Title: Models of Homotopy Type Theory with an Interval Type

Valery Isaev

Comments: 7 pages

Subjects: Logic in Computer Science (cs.LO)

[67] arXiv:2004.14378 [pdf, other]

Title: Towards Faster Reasoners By Using Transparent Huge Pages

Johannes K. Fichte, Norbert Manthey, Julian Stecklina, André Schidler

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

[68] arXiv:2004.14561 [pdf, other]

Title: An Axiomatic Approach to Existence and Liveness for Differential Equations

Yong Kiam Tan, André Platzer

Comments: Significantly extended version of arXiv:1904.07984

Journal-ref: Formal Aspects of Computing 33, pp. 461-518, 2021

Subjects: Logic in Computer Science (cs.LO)

[69] arXiv:2004.14750 [pdf, other]

Title: Proceedings 16th International Conference on Quantum Physics and Logic

Bob Coecke (University of Oxford), Matthew Leifer (Chapman University)

Journal-ref: EPTCS 318, 2020

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

[70] arXiv:2004.14835 [pdf, other]

Title: PrIC3: Property Directed Reachability for MDPs

Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer

Subjects: Logic in Computer Science (cs.LO)

[71] arXiv:2004.14931 [pdf, other]

Title: The Complexity of Dynamic Data Race Prediction

Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan

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

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

Title: An abstract semantics of speculative execution for reasoning about security vulnerabilities

Robert J. Colvin, Kirsten Winter

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

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

Title: Mixed Sessions: the Other Side of the Tape

Filipe Casal (LASIGE, Faculdade de Ciências, Universidade de Lisboa, Portugal), Andreia Mordido (LASIGE, Faculdade de Ciências, Universidade de Lisboa, Portugal), Vasco T. Vasconcelos (LASIGE, Faculdade de Ciências, Universidade de Lisboa, Portugal)

Comments: In Proceedings PLACES 2020, arXiv:2004.01062

Journal-ref: EPTCS 314, 2020, pp. 46-60

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

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

Title: Verifying Recurrent Neural Networks using Invariant Inference

Yuval Jacoby, Clark Barrett, Guy Katz

Comments: This is the extended version of a paper with the same title that appeared at ATVA 2020

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

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

Title: Continuous Motion Planning with Temporal Logic Specifications using Deep Neural Networks

Chuanzheng Wang, Yinan Li, Stephen L. Smith, Jun Liu

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

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

Title: On Evaluating the Quality of Rule-Based Classification Systems

Nassim Dehouche

Comments: ICIC Express Letters Volume 11, Number 10, October 2017

Journal-ref: ICIC Express Letters ICIC International c 2013 ISSN 1881-803X ICIC Express Letters Volume 11, Number 10, October 2017 c 2013 ISSN 1881-803X Volume 11, Number 10, October 2017

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

[77] arXiv:2004.02770 (cross-list from cs.CR) [pdf, other]

Title: Establishing Cyber Resilience in Embedded Systems for Securing Next-Generation Critical Infrastructure

Fahad Siddiqui, Matthew Hagan, Sakir Sezer

Comments: 6 pages, 1 figure, 1 table

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

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

Title: Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL

Sadegh Dalvandi, Brijesh Dongol, Simon Doherty

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

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

Title: Decidability and Synthesis of Abstract Inductive Invariants

Francesco Ranzato

Journal-ref: Proceedings of CONCUR 2020

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

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

Title: A categorical approach to secure compilation

Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens

Comments: Accepted in Coalgebraic Methods in Computer Science, ver. 2020

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

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

Title: A Structural Approach to Dynamic Migration in Petri Net Models of Structured Workflows

Ahana Pradhan, Rushikesh K. Joshi

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

[82] arXiv:2004.04034 (cross-list from cs.SC) [pdf, other]

Title: New Opportunities for the Formal Proof of Computational Real Geometry?

Erika {Á}brahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks

Journal-ref: Proceedings of the 5th Workshop on Satisfiability Checking and Symbolic Computation (SC2 '20), CEUR Workshop Proceedings 2752, pp. 178-188, 2020

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

[83] arXiv:2004.04128 (cross-list from cs.CL) [pdf, other]

Title: Putting a Spin on Language: A Quantum Interpretation of Unary Connectives for Linguistic Applications

Adriana D. Correia (Utrecht University), Henk T. C. Stoof (Utrecht University), Michael Moortgat (Utrecht University)

Comments: In Proceedings QPL 2020, arXiv:2109.01534

Journal-ref: EPTCS 340, 2021, pp. 114-140

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

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

Title: Slicing and dicing soccer: automatic detection of complex events from spatio-temporal data

Lia Morra, Francesco Manigrasso, Giuseppe Canto, Claudio Gianfrate, Enrico Guarino, Fabrizio Lamberti

Comments: accepted at 17th International Conference on Image Analysis and Recognition ICIAR 2020

Subjects: Computer Vision and Pattern Recognition (cs.CV); Logic in Computer Science (cs.LO)

[85] arXiv:2004.04526 (cross-list from math.CT) [pdf, other]

Title: Open Diagrams via Coend Calculus

Mario Román (Tallinn University of Technology)

Comments: Formatting revision after Proceedings ACT 2020, minor changes

Journal-ref: EPTCS 333, 2021, pp. 65-78

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

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

Title: Parameterized Verification of Systems with Global Synchronization and Guards

Nouraldin Jaber (1), Swen Jacobs (2), Christopher Wagner (1), Milind Kulkarni (1), Roopsha Samanta (1) ((1) Purdue University, (2) CISPA Helmholtz Center for Information Security)

Comments: Conference version published at CAV 2020; this version contains a correction of guard-compatibility conditions C2.1 and C2.2

Journal-ref: Lecture Notes in Computer Science, vol 12224. Springer (2020)

Subjects: Formal Languages and Automata Theory (cs.FL); Distributed, Parallel, and Cluster Computing (cs.DC); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

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

Title: Cores over Ramsey structures

Antoine Mottet, Michael Pinsker

Comments: 9 pages

Journal-ref: J. symb. log. 86 (2021) 352-361

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

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

Title: A Higher Structure Identity Principle

Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis

Comments: Long version of publication in LICS 2020 (DOI: https://doi.org/10.1145/3373718.3394755%29%3B v2: added sections "Axioms and Theories" and "Version History", other minor changes; v3: added examples

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

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

Title: Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates

Emanuele De Angelis (1 and 3), Fabio Fioravanti (1), Alberto Pettorossi (2 and 3), Maurizio Proietti (3) ((1) DEC, University G. D'Annunzio, Pescara, Italy, (2) DICII, University of Rome Tor Vergata, Roma, Italy, (3) CNR-IASI, Roma, Italy)

Comments: 10th International Joint Conference on Automated Reasoning (IJCAR 2020) - version with appendix; added DOI of the final authenticated Springer publication; minor corrections

Journal-ref: Lecture Notes in Computer Science, vol 12166. Springer, Cham, 2020, pp. 83-102

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

[90] arXiv:2004.08200 (cross-list from cs.DC) [pdf, other]

Title: Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory

Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim

Comments: This is the full version of the paper that is to appear in FORTE 2020 (this https URL)

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

[91] arXiv:2004.08487 (cross-list from math.CT) [pdf, other]

Title: *-Autonomous Envelopes and Conservativity

Michael Shulman (University of San Diego)

Comments: In Proceedings Linearity&TLLA 2020, arXiv:2112.14305

Journal-ref: EPTCS 353, 2021, pp. 175-194

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

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

Title: Three Modern Roles for Logic in AI

Adnan Darwiche

Comments: To be published in PODS 2020

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

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

Title: Make E Smart Again

Zarathustra Amadeus Goertzel

Comments: 8 pages, 2 figures, IJCAR2020

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

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

Title: Characterizing Boundedness in Chase Variants

Stathis Delivorias, Michel Leclère, Marie-Laure Mugnier, Federico Ulliana

Comments: Under consideration for publication in Theory and Practice of Logic Programming

Journal-ref: Theory and Practice of Logic Programming 21 (2021) 51-79

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

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

Title: Categories of Semantic Concepts

James Hefford, Vincent Wang, Matthew Wilson

Comments: Accepted at SemSpace 2020

Subjects: Computation and Language (cs.CL); Logic in Computer Science (cs.LO); Category Theory (math.CT); Quantum Physics (quant-ph)

[96] arXiv:2004.11196 (cross-list from econ.TH) [pdf, other]

Title: The Category of Node-and-Choice Extensive-Form Games

Peter A. Streufert

Comments: 49 pages, 10 figures; revision makes only expositional changes (an improved introduction and a new running example)

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

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

Title: QueryVis: Logic-based diagrams help users understand complicated SQL queries faster

Aristotelis Leventidis, Jiahui Zhang, Cody Dunne, Wolfgang Gatterbauer, H.V. Jagadish, Mirek Riedewald

Comments: Full version of paper appearing in SIGMOD 2020

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

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

Title: Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version)

Julia Gabet, Nobuko Yoshida

Comments: Short version of this paper published in: ECOOP 2020; 26 pages + references and appendix; Main body: 17 figures + 1 table; Appendix: 1 figure

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

[99] arXiv:2004.12921 (cross-list from quant-ph) [pdf, other]

Title: Equivalence of Grandfather and Information Antinomy Under Intervention

Ämin Baumeler, Eleftherios Tselentis

Comments: In Proceedings QPL 2020, arXiv:2109.01534

Journal-ref: EPTCS 340, 2021, pp. 1-12

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

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

Title: An ASP-Based Approach to Counterfactual Explanations for Classification

Leopoldo Bertossi

Comments: Revised and extended version. To appear in Proc. RuleML+RR, 2020

Subjects: Machine Learning (cs.LG); Databases (cs.DB); Logic in Computer Science (cs.LO); Machine Learning (stat.ML)

[101] arXiv:2004.13285 (cross-list from cs.NI) [pdf, other]

Title: Formalising the Optimised Link State Routing Protocol

Ryan Barry, Rob van Glabbeek, Peter Höfner

Comments: In Proceedings MARS 2020, arXiv:2004.12403

Journal-ref: EPTCS 316, 2020, pp. 40-71

Subjects: Networking and Internet Architecture (cs.NI); Logic in Computer Science (cs.LO)

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

Title: Formal Models of the OSPF Routing Protocol

Jack Drury, Peter Höfner, Weiyou Wang

Comments: In Proceedings MARS 2020, arXiv:2004.12403

Journal-ref: EPTCS 316, 2020, pp. 72-120

Subjects: Networking and Internet Architecture (cs.NI); Logic in Computer Science (cs.LO)

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

Title: Linear Dependent Type Theory for Quantum Programming Languages

Peng Fu, Kohei Kishida, Peter Selinger

Journal-ref: Logical Methods in Computer Science, Volume 18, Issue 3 (September 7, 2022) lmcs:6930

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO); Category Theory (math.CT); Quantum Physics (quant-ph)

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

Title: Compilation of Coordinated Choice

Yuki Nishida, Atsushi Igarashi

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

[105] arXiv:2004.14384 (cross-list from eess.SY) [pdf, other]

Title: A Formally Verified HOL4 Algebra for Event Trees

Mohamed Abdelghany, Waqar Ahmad, Sofiene Tahar

Comments: 17 pages, 3 figures

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

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

Title: Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice

Kuldeep S. Meel, S. Akshay

Comments: Full version of paper accepted in LICS2020 conference

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

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

Title: Twin-width I: tractable FO model checking

Édouard Bonnet, Eun Jung Kim, Stéphan Thomassé, Rémi Watrigant

Comments: 49 pages, 9 figures

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

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

Title: Do Neural Models Learn Systematicity of Monotonicity Inference in Natural Language?

Hitomi Yanaka, Koji Mineshima, Daisuke Bekki, Kentaro Inui

Comments: accepted by ACL2020 as a long paper

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

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

Title: Local State Space Analysis to Assist Partial Order Reduction

Hao Zheng, Yingying Zhang, Chris Myers

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