Logic in Computer Science

Authors and titles for cs.LO in Jul 2021

[1]  arXiv:2107.00086 [pdf, ps, other]

Title: An extended and more practical mwp flow analysis

Authors: Clément Aubert, Thomas Rubiano (LIPN), Neea Rusch, Thomas Seiller (LIPN, CNRS)

Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC); Programming Languages (cs.PL); Logic (math.LO)

[2]  arXiv:2107.00111 [pdf, ps, other]

Title: A Logic for Reasoning About LF Specifications

Authors: Gopalan Nadathur, Mary Southern

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

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

[3]  arXiv:2107.00319 [pdf, other]

Title: Addressing Machines as models of lambda-calculus

Authors: Giuseppe Della Penna, Benedetto Intrigila, Giulio Manzonetto

Journal-ref: Logical Methods in Computer Science, Volume 18, Issue 3 (July 29, 2022) lmcs:7645

Subjects: Logic in Computer Science (cs.LO)

[4]  arXiv:2107.00369 [pdf, ps, other]

Title: Computing CQ lower-bounds over OWL 2 through approximation to RSA

Authors: Federico Igne, Stefano Germano, Ian Horrocks

Comments: 26 pages, 1 figure

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

[5]  arXiv:2107.00612 [pdf, other]

Title: Formal verification of octorotor flight envelope using barrier functions and SMT solving

Authors: Byron Heersink, Pape Sylla, Michael A. Warren

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

[6]  arXiv:2107.00804 [pdf, ps, other]

Title: Formal Semantics of a Classical-Quantum Language

Authors: Yuxin Deng, Yuan Feng

Comments: 30 pages

Subjects: Logic in Computer Science (cs.LO)

[7]  arXiv:2107.00929 [pdf, other]

Title: Incorporating Monitors in Reactive Synthesis without Paying the Price

Authors: Shaun Azzopardi, Nir Piterman, Gerardo Schneider

Subjects: Logic in Computer Science (cs.LO)

[8]  arXiv:2107.01136 [pdf, ps, other]

Title: Live Synthesis

Authors: Bernd Finkbeiner, Felix Klein, Niklas Metzger

Subjects: Logic in Computer Science (cs.LO)

[9]  arXiv:2107.01155 [pdf, ps, other]

Title: Higher-order probabilistic adversarial computations: Categorical semantics and program logics

Authors: Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato

Comments: Full version of ICFP 21 paper

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

[10]  arXiv:2107.01468 [pdf, ps, other]

Title: First-Order logic and its Infinitary Quantifier Extensions over Countable Words

Authors: Bharat Adsul, Saptarshi Sarkar, A.V. Sreejith

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

[11]  arXiv:2107.01542 [pdf, ps, other]

Title: The Semantics of Package Management via Event Structures

Authors: Gershom Bazerman

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

[12]  arXiv:2107.01544 [pdf, ps, other]

Title: Proceedings Seventh Workshop on Proof eXchange for Theorem Proving

Authors: Chantal Keller (JKU Linz), Mathias Fleury (LRI, Université Paris Saclay, and CNRS)

Journal-ref: EPTCS 336, 2021

Subjects: Logic in Computer Science (cs.LO)

[13]  arXiv:2107.01594 [pdf, other]

Title: A Rewriting Coherence Theorem with Applications in Homotopy Type Theory

Authors: Nicolai Kraus, Jakob von Raumer

Comments: 34 pages; expands on and reuses material of our previous conference paper "Coherence via Well-Foundedness", arXiv:2001.07655

Journal-ref: Mathematical Structures in Computer Science, 1-33, 2023

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

[14]  arXiv:2107.01687 [pdf, other]

Title: Linear-Time Model Checking Branching Processes

Authors: Stefan Kiefer, Pavel Semukhin, Cas Widdershoven

Comments: full version of a CONCUR'21 paper

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

[15]  arXiv:2107.01815 [pdf, other]

Title: A Formal Semantics of the GraalVM Intermediate Representation

Authors: Brae J. Webb, Mark Utting, Ian J. Hayes

Comments: 16 pages, 8 figures, to be published to ATVA 2021

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

[16]  arXiv:2107.01998 [pdf, ps, other]

Title: Nested Sequents for Intuitionistic Modal Logics via Structural Refinement

Authors: Tim S. Lyon

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

[17]  arXiv:2107.02203 [pdf, other]

Title: Automated inference of production rules for glycans

Authors: Ansuman Biswas, Ashutosh Gupta, Meghana Missula, Mukund Thattai

Comments: 23 pages; 2 figures

Subjects: Logic in Computer Science (cs.LO)

[18]  arXiv:2107.02333 [pdf, ps, other]

Title: Symbol Elimination for Parametric Second-Order Entailment Problems (with Applications to Problems in Wireless Network Theory)

Authors: Dennis Peuter, Philipp Marohn, Viorica Sofronie-Stokkermans

Comments: 44 pages

Subjects: Logic in Computer Science (cs.LO)

[19]  arXiv:2107.02351 [pdf, ps, other]

Title: Proof Generation in CDSAT

Authors: Maria Paola Bonacina (Università degli Studi di Verona, Italy)

Comments: In Proceedings PxTP 2021, arXiv:2107.01544

Journal-ref: EPTCS 336, 2021, pp. 1-4

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

[20]  arXiv:2107.02352 [pdf, other]

Title: A Framework for Proof-carrying Logical Transformations

Authors: Quentin Garchery

Comments: In Proceedings PxTP 2021, arXiv:2107.01544

Journal-ref: EPTCS 336, 2021, pp. 5-23

Subjects: Logic in Computer Science (cs.LO)

[21]  arXiv:2107.02353 [pdf, ps, other]

Title: General Automation in Coq through Modular Transformations

Authors: Valentin Blot (LMF, Inria, Université Paris-Saclay), Louise Dubois de Prisque (LMF, Inria, Université Paris-Saclay), Chantal Keller (LMF, Université Paris-Saclay), Pierre Vial (LMF, Inria, Université Paris-Saclay)

Comments: In Proceedings PxTP 2021, arXiv:2107.01544

Journal-ref: EPTCS 336, 2021, pp. 24-39

Subjects: Logic in Computer Science (cs.LO)

[22]  arXiv:2107.02354 [pdf, other]

Title: Alethe: Towards a Generic SMT Proof Format (extended abstract)

Authors: Hans-Jörg Schurr (University of Lorraine, CNRS, Inria, and LORIA), Mathias Fleury (Johannes Kepler University Linz), Haniel Barbosa (Universidade Federal de Minas Gerais), Pascal Fontaine (University of Liège)

Comments: In Proceedings PxTP 2021, arXiv:2107.01544

Journal-ref: EPTCS 336, 2021, pp. 49-54

Subjects: Logic in Computer Science (cs.LO)

[23]  arXiv:2107.02509 [pdf, other]

Title: A Temporal Logic for Strategic Hyperproperties

Authors: Raven Beutner, Bernd Finkbeiner

Comments: Full Version for CONCUR 2021

Subjects: Logic in Computer Science (cs.LO)

[24]  arXiv:2107.03155 [pdf, ps, other]

Title: The Quantitative Collapse of Concurrent Games with Symmetry

Authors: Pierre Clairambault (LIP, PLUME), Hugo Paquet

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

[25]  arXiv:2107.03189 [pdf, other]

Title: A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic

Authors: Martin Bromberger (1), Irina Dragoste (2), Rasha Faqeh (2), Christof Fetzer (2), Markus Krötzsch (2), Christoph Weidenbach (1) ((1) Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany, (2) TU Dresden, Dresden, Germany)

Comments: 26 pages

Subjects: Logic in Computer Science (cs.LO)

[26]  arXiv:2107.03711 [pdf, other]

Title: Stable graphs of bounded twin-width

Authors: Jakub Gajarský, Michał Pilipczuk, Szymon Toruńczyk

Comments: 45 pages, 5 figures

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

[27]  arXiv:2107.03778 [src]

Title: Choiceless Polynomial Time, Symmetric Circuits and Cai-Fürer-Immerman Graphs

Authors: Benedikt Pago

Comments: replaced with a substantially improved and augmented version

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

[28]  arXiv:2107.03794 [pdf, ps, other]

Title: The Satisfiability Problem for a Quantitative Fragment of PCTL

Authors: Miroslav Chodil, Antonín Kučera

Subjects: Logic in Computer Science (cs.LO)

[29]  arXiv:2107.04298 [pdf, ps, other]

Title: An Algorithm for Reversible Logic Circuit Synthesis Based on Tensor Decomposition

Authors: Hochang Lee, Kyung Chul Jeong, Daewan Han, Panjin Kim

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

[30]  arXiv:2107.05253 [pdf, ps, other]

Title: Reasoning about Reconfigurations of Distributed Systems

Authors: Emma Ahrens, Marius Bozga, Radu Iosif, Joost-Pieter Katoen

Subjects: Logic in Computer Science (cs.LO)

[31]  arXiv:2107.05261 [pdf, ps, other]

Title: Coherent differentiation

Authors: Thomas Ehrhard (IRIF (UMR\_8243))

Subjects: Logic in Computer Science (cs.LO)

[32]  arXiv:2107.05285 [pdf, ps, other]

Title: Separating Data Examples by Description Logic Concepts with Restricted Signatures

Authors: Jean Christoph Jung, Carsten Lutz, Hadrien Pulcini, Frank Wolter

Comments: A short version of this paper has been accepted for publication in the Proceedings of KR 2021

Subjects: Logic in Computer Science (cs.LO)

[33]  arXiv:2107.05296 [pdf, ps, other]

Title: Separating LREC from LFP

Authors: Anuj Dawar, Felipe Ferreira Santos

Comments: 21 pages. Submitted

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

[34]  arXiv:2107.05378 [pdf, other]

Title: Tableaux like model checking on-the-fly for ATL+

Authors: Serenella Cerrito

Comments: 29 pages

Subjects: Logic in Computer Science (cs.LO)

[35]  arXiv:2107.05493 [pdf, other]

Title: Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant

Authors: Nicolas Magaud (ICube - Université de Strasbourg)

Comments: In Proceedings PxTP 2021, arXiv:2107.01544

Journal-ref: EPTCS 336, 2021, pp. 40-47

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

[36]  arXiv:2107.05928 [pdf, other]

Title: First-Order Logic with Connectivity Operators

Authors: Nicole Schirrmacher, Sebastian Siebertz, Alexandre Vigny

Comments: 18 pages, 3 figures

Subjects: Logic in Computer Science (cs.LO)

[37]  arXiv:2107.06042 [pdf, other]

Title: Finite Model Property and Bisimulation for LFD

Authors: Raoul Koudijs

Comments: 15 pages, submitted for GandALF 2021 conference

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

[38]  arXiv:2107.06045 [pdf, ps, other]

Title: Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic

Authors: Eric Campbell, Michael Greenberg

Subjects: Logic in Computer Science (cs.LO)

[39]  arXiv:2107.06075 [pdf, ps, other]

Title: A Rational Entailment for Expressive Description Logics via Description Logic Programs

Authors: Giovanni Casini, Umberto Straccia

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

[40]  arXiv:2107.06084 [pdf, other]

Title: Decentralized LTL Enforcement

Authors: Florian Gallay (Univ. Grenoble Alpes, CNRS, Inria, Grenoble INP, Laboratoire d'Informatique de Grenoble, 38000 Grenoble, France), Yliès Falcone (Univ. Grenoble Alpes, CNRS, Inria, Grenoble INP, Laboratoire d'Informatique de Grenoble, 38000 Grenoble, France)

Comments: In Proceedings GandALF 2021, arXiv:2109.07798

Journal-ref: EPTCS 346, 2021, pp. 135-151

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

[41]  arXiv:2107.06150 [pdf, ps, other]

Title: From Identity to Difference: A Quantitative Interpretation of the Identity Type

Authors: Paolo Pistone

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

[42]  arXiv:2107.06152 [pdf, ps, other]

Title: A model of systems with modes and mode transitions

Authors: Edwin Beggs, John V. Tucker

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

[43]  arXiv:2107.06591 [pdf, ps, other]

Title: Useful Open Call-by-Need

Authors: Beniamino Accattoli, Maico Leberle

Comments: This is the version with proofs of the paper with the same title and authors in the proceedings of CSL 2022

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

[44]  arXiv:2107.06672 [pdf, ps, other]

Title: Improved SAT models for NFA learning

Authors: Frédéric Lardeux (LERIA), Eric Monfroy (LERIA)

Journal-ref: International Conference in Optimization and Learning (OLA), Jun 2021, Catania, Italy

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

[45]  arXiv:2107.07228 [pdf, ps, other]

Title: Tableaux for Free Logics with Descriptions

Authors: Andrzej Indrzejczak, Michał Zawidzki

Comments: This is a full version of a conference paper that will appear in the proceedings of the 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX)

Subjects: Logic in Computer Science (cs.LO)

[46]  arXiv:2107.07376 [pdf, ps, other]

Title: Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

Authors: Elaine Pimentel (UFRN), Enrico Tassi (Inria)

Journal-ref: EPTCS 337, 2021

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

[47]  arXiv:2107.07661 [pdf, other]

Title: Facilitating Meta-Theory Reasoning (Invited Paper)

Authors: Giselle Reis (Carnegie Mellon University)

Comments: In Proceedings LFMTP 2021, arXiv:2107.07376

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

Subjects: Logic in Computer Science (cs.LO)

[48]  arXiv:2107.07662 [pdf, ps, other]

Title: Interacting Safely with an Unsafe Environment

Authors: Gilles Dowek (Inria and ENS Paris-Saclay)

Comments: In Proceedings LFMTP 2021, arXiv:2107.07376

Journal-ref: EPTCS 337, 2021, pp. 30-38

Subjects: Logic in Computer Science (cs.LO)

[49]  arXiv:2107.07663 [pdf, ps, other]

Title: Countability of Inductive Types Formalized in the Object-Logic Level

Authors: Qinxiang Cao (John Hopcroft Center of Computer Science, Shanghai Jiao Tong University, Shanghai Key Laboratory of Trustworthy Computing, East China Normal University), Xiwei Wu (Shanghai Jiao Tong University)

Comments: In Proceedings LFMTP 2021, arXiv:2107.07376

Journal-ref: EPTCS 337, 2021, pp. 55-70

Subjects: Logic in Computer Science (cs.LO)

[50]  arXiv:2107.07664 [pdf, other]

Title: SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts

Authors: Laila El-Beheiry (Carnegie Mellon University), Giselle Reis (Carnegie Mellon University), Ammar Karkour (Carnegie Mellon University)

Comments: In Proceedings LFMTP 2021, arXiv:2107.07376

Journal-ref: EPTCS 337, 2021, pp. 71-87

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

[51]  arXiv:2107.07665 [pdf, ps, other]

Title: Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style

Authors: Florian Rabe (University Erlangen-Nuremberg), Navid Roux (University Erlangen-Nuremberg)

Comments: In Proceedings LFMTP 2021, arXiv:2107.07376

Journal-ref: EPTCS 337, 2021, pp. 88-103

Subjects: Logic in Computer Science (cs.LO)

[52]  arXiv:2107.07666 [pdf, ps, other]

Title: Adelfa: A System for Reasoning about LF Specifications

Authors: Mary Southern (University of Minnesota), Gopalan Nadathur (University of Minnesota)

Comments: In Proceedings LFMTP 2021, arXiv:2107.07376

Journal-ref: EPTCS 337, 2021, pp. 104-120

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

[53]  arXiv:2107.07669 [pdf, ps, other]

Title: Automating Induction by Reflection

Authors: Johannes Schoisswohl (University of Manchester), Laura Kovács (TU Wien)

Comments: In Proceedings LFMTP 2021, arXiv:2107.07376. A full version of this paper appears at arXiv:2106.05066

Journal-ref: EPTCS 337, 2021, pp. 39-54

Subjects: Logic in Computer Science (cs.LO)

[54]  arXiv:2107.07726 [pdf, other]

Title: Double Glueing over Free Exponential: with Measure Theoretic Applications

Authors: Masahiro Hamano

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

[55]  arXiv:2107.07811 [pdf, ps, other]

Title: Capturing Homomorphism-Closed Decidable Queries with Existential Rules

Authors: Camille Bourgaux, David Carral, Markus Krötzsch, Sebastian Rudolph, Michaël Thomazo

Comments: Technical Report of our KR 2021 Paper

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

[56]  arXiv:2107.08253 [pdf, other]

Title: A proof theoretic basis for relational semantics

Authors: Carlos G. Lopez Pombo, Thomas S.E. Maibaum

Comments: Many overflows I will solve in the future. Submitted for review to Journal of Logic and Computation

Subjects: Logic in Computer Science (cs.LO)

[57]  arXiv:2107.08349 [pdf, other]

Title: Proof Search on Bilateralist Judgments over Non-deterministic Semantics

Authors: Vitor Greati, Sérgio Marcelino, João Marcos

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

[58]  arXiv:2107.08409 [pdf, other]

Title: AC Simplifications and Closure Redundancies in the Superposition Calculus

Authors: André Duarte, Konstantin Korovin

Comments: Full version of the paper to appear in TABLEAUX 2021

Subjects: Logic in Computer Science (cs.LO)

[59]  arXiv:2107.08453 [pdf, ps, other]

Title: Probabilistic Process Algebra for True Concurrency

Authors: Yong Wang

Comments: 139 pages, 60 tables. arXiv admin note: substantial text overlap with arXiv:1611.09035, arXiv:2101.05140, arXiv:2104.05438, arXiv:1810.00868, arXiv:1907.02668, arXiv:1811.01070, arXiv:1501.05260, arXiv:1404.0665

Subjects: Logic in Computer Science (cs.LO)

[60]  arXiv:2107.08728 [pdf, ps, other]

Title: Cobordisms and commutative categorial grammars

Authors: Sergey Slavnov

Comments: This is the final version of the previously posted series of drafts on cobordimns and categorial grammars. Concise and, hopefully, much improved presentation, but no new mathematical content compared to preceding versions. arXiv admin note: text overlap with arXiv:1911.03962

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

[61]  arXiv:2107.08794 [pdf, other]

Title: GenSys: A Scalable Fixed-point Engine for Maximal Controller Synthesis over Infinite State Spaces

Authors: Stanly Samuel, Deepak D'Souza, Raghavan Komondoor

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

[62]  arXiv:2107.08852 [pdf, ps, other]

Title: Structured Proofs for Adversarial Cyber-Physical Systems

Authors: Rose Bohrer, André Platzer

Comments: Preprint of paper appearing in ESWEEK-TECS (EMSOFT 2021)

Journal-ref: ACM Trans. Embed. Comput. Syst. 20(5s), 2021

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

[63]  arXiv:2107.08921 [pdf, ps, other]

Title: Dormancy-aware timed branching bisimilarity, with an application to communication protocol analysis

Authors: C. A. Middelburg

Comments: 39 pages, revision of v3, presentation improved at several places

Subjects: Logic in Computer Science (cs.LO)

[64]  arXiv:2107.09280 [pdf, other]

Title: Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory (Full Version)

Authors: Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog

Subjects: Logic in Computer Science (cs.LO)

[65]  arXiv:2107.10034 [pdf, other]

Title: Learning Theorem Proving Components

Authors: Karel Chvalovský, Jan Jakubův, Miroslav Olšák, Josef Urban

Comments: Accepted to TABLEAUX'21

Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Neural and Evolutionary Computing (cs.NE); Symbolic Computation (cs.SC)

[66]  arXiv:2107.10188 [pdf, ps, other]

Title: JEFL: Joint Embedding of Formal Proof Libraries

Authors: Qingxiang Wang, Cezary Kaliszyk

Comments: Submission to FroCoS 2021

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

[67]  arXiv:2107.10832 [pdf, ps, other]

Title: A Logic of Expertise

Authors: Joseph Singleton

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

[68]  arXiv:2107.10988 [pdf, other]

Title: Formalizing Galois Theory

Authors: Thomas Browning, Patrick Lutz

Comments: 15 pages

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

[69]  arXiv:2107.11280 [pdf, other]

Title: Type-based Enforcement of Infinitary Trace Properties for Java

Authors: Serdar Erbatur, Ulrich Schöpp, Chuangjie Xu

Comments: main part (14 pages) published at PPDP'21; arXiv version contains an appendix on the FJ operational semantics and the extension to support exception handling (15 pages total)

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

[70]  arXiv:2107.11674 [pdf, other]

Title: Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS

Authors: Lorenzo Gheri, Andrei Popescu

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

[71]  arXiv:2107.11679 [pdf, ps, other]

Title: Reasoning about Recursive Quantum Programs

Authors: Zhaowei Xu, Mingsheng Ying, Benoît Valiron

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

[72]  arXiv:2107.11841 [pdf, ps, other]

Title: Model Checking Algorithms for Hyperproperties

Authors: Bernd Finkbeiner

Subjects: Logic in Computer Science (cs.LO)

[73]  arXiv:2107.12475 [pdf, other]

Title: On the hardness of knowing busy beaver values BB(15) and BB(5,4)

Authors: Tristan Stérin, Damien Woods

Comments: 12 pages, 5 figures, code and machines available at this https URL

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

[74]  arXiv:2107.12902 [pdf, ps, other]

Title: Logical Characterization of Coherent Uninterpreted Programs

Authors: Hari Govind V K, Sharon Shoham, Arie Gurfinkel

Comments: Accepted at FMCAD 2021

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

[75]  arXiv:2107.13242 [pdf, ps, other]

Title: Type theories in category theory

Authors: Tesla Zhang

Comments: 47 pages

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

[76]  arXiv:2107.13347 [pdf, ps, other]

Title: Semantics for Variational Quantum Programming

Authors: Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, Vladimir Zamdzhiev

Journal-ref: Proc. ACM Program. Lang. 6, POPL, Article 26 (January 2022)

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

[77]  arXiv:2107.13477 [pdf, other]

Title: Satisfiability and Synthesis Modulo Oracles

Authors: Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia

Comments: 12 pages, 8 Figures

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

[78]  arXiv:2107.13953 [pdf, other]

Title: Separator logic and star-free expressions for graphs

Authors: Mikolaj Bojanczyk

Subjects: Logic in Computer Science (cs.LO)

[79]  arXiv:2107.13975 [pdf, ps, other]

Title: A Sketch of a Proof-Theoretic Semantics for Necessity

Authors: Nils Kürbis

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

[80]  arXiv:2107.13988 [pdf, ps, other]

Title: Proof-Theoretic Semantics, a Problem with Negation and Prospects for Modality

Authors: Nils Kürbis

Journal-ref: Journal of Philosophical Logic 44/6 (2015): 713-727

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

[81]  arXiv:2107.14283 [pdf, ps, other]

Title: Syllepsis in Homotopy Type Theory

Authors: Kristina Sojakova

Subjects: Logic in Computer Science (cs.LO)

[82]  arXiv:2107.14487 [pdf, other]

Title: Refining Labelled Systems for Modal and Constructive Logics with Applications

Authors: Tim Lyon

Comments: PhD Thesis

Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Discrete Mathematics (cs.DM); Formal Languages and Automata Theory (cs.FL); Logic (math.LO)

[83]  arXiv:2107.14651 [pdf, ps, other]

Title: Minimal Translations from Synchronous Communication to Synchronizing Locks (Extended Version)

Authors: Manfred Schmidt-Schauß, David Sabel

Subjects: Logic in Computer Science (cs.LO)

[84]  arXiv:2107.14668 [pdf, ps, other]

Title: Interleaving & Reconfigurable Interaction: Separating Choice from Scheduling using Glue

Authors: Yehia Abd Alrahman, Mauricio Martel, Nir Piterman

Comments: This work is funded by the ERC consolidator grant D-SynMA (No. 772459) and the Swedish research council grants: SynTM (No.2020-03401) and VR project (No. 2020-04963)

Subjects: Logic in Computer Science (cs.LO)

[85]  arXiv:2107.00032 (cross-list from cs.MA) [pdf, other]

Title: Agree to Disagree: Subjective Fairness in Privacy-Restricted Decentralised Conflict Resolution

Authors: Alex Raymond, Matthew Malencia, Guilherme Paulino-Passos, Amanda Prorok

Comments: 25 pages, 8 figures

Journal-ref: Frontiers of Robotics and AI, 2022

Subjects: Multiagent Systems (cs.MA); Logic in Computer Science (cs.LO); Robotics (cs.RO)

[86]  arXiv:2107.00097 (cross-list from cs.PL) [pdf, ps, other]

Title: pymwp: A Tool for Guaranteeing Complexity Bounds for C Programs

Authors: Clément Aubert, Thomas Rubiano (LIPN), Neea Rusch, Thomas Seiller (LIPN, CNRS)

Subjects: Programming Languages (cs.PL); Computational Complexity (cs.CC); Logic in Computer Science (cs.LO); Logic (math.LO)

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

Title: Anti-unification of Unordered Goals

Authors: Gonzague Yernaux, Wim Vanhoof

Comments: CSL 2022 paper with appendices

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

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

Title: Evidence for Long-Tails in SLS Algorithms

Authors: Florian Wörz, Jan-Hendrik Lorenz

Comments: To appear at ESA 2021

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

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

Title: Verifying Verified Code

Authors: Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel

Comments: 24 pages, 17 figures, to be included in ATVA 2021 conference proceedings

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

[90]  arXiv:2107.01428 (cross-list from cs.AI) [pdf, ps, other]

Title: Solving Infinite-Domain CSPs Using the Patchwork Property

Authors: Konrad K. Dabrowski, Peter Jonsson, Sebastian Ordyniak, George Osipov

Comments: 34 pages, 2 figures. Parts of this article appeared in the proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI 2021)

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

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

Title: Faster-LTN: a neuro-symbolic, end-to-end object detection architecture

Authors: Francesco Manigrasso, Filomeno Davide Miro, Lia Morra, Fabrizio Lamberti

Comments: accepted for presentation at ICANN 2021

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

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

Title: A Theory of Higher-Order Subtyping with Type Intervals (Extended Version)

Authors: Sandro Stucki, Paolo G. Giarrusso

Comments: 73 pages; to be presented at the 26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021), 22-27 August 2021

Journal-ref: Proc. ACM Program. Lang. 5 (2021) 69:1-69:30 (ICFP)

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

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

Title: Proving SIFA Protection of Masked Redundant Circuits

Authors: Vedad Hadzic, Robert Primas, Roderick Bloem

Comments: This is the extended version of the paper published at ATVA 2021

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

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

Title: On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets

Authors: Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, James Worrell

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

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

Title: Probabilistic Trace Alignment

Authors: Giacomo Bergami, Fabrizio Maria Maggi, Marco Montali, Rafael Peñaloza

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

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

Title: An ontology for the formalization and visualization of scientific knowledge

Authors: Vincenzo Daponte, Gilles Falquet

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

[97]  arXiv:2107.05225 (cross-list from cs.PL) [pdf, ps, other]

Title: Compositional Vulnerability Detection with Insecurity Separation Logic (Extended Version)

Authors: Toby Murray, Pengbo Yan, Gidon Ernst

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

[98]  arXiv:2107.06121 (cross-list from cs.CC) [pdf, ps, other]

Title: The Dynamic Complexity of Acyclic Hypergraph Homomorphisms

Authors: Nils Vortmeier, Ioannis Kokkinis

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

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

Title: Maintaining $\mathsf{CMSO}_2$ properties on dynamic structures with bounded feedback vertex number

Authors: Konrad Majewski, Michał Pilipczuk, Marek Sokołowski

Comments: 80 pages, 5 figures

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

[100]  arXiv:2107.06329 (cross-list from cs.AI) [pdf, ps, other]

Title: Efficient exact computation of the conjunctive and disjunctive decompositions of D-S Theory for information fusion: Translation and extension

Authors: Maxime Chaveroche, Franck Davoine, Véronique Cherfaoui

Comments: Extension of an article published in the proceedings of the french conference GRETSI 2019

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

[101]  arXiv:2107.06727 (cross-list from cs.FL) [pdf, ps, other]

Title: Composition of choreography automata

Authors: Franco Barbanera, Ivan Lanese, Emilio Tuosto

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

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

Title: Forgetting in Answer Set Programming -- A Survey

Authors: Ricardo Gonçalves, Matthias Knorr, João Leite

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

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

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

Title: Touring the MetaCoq Project (Invited Paper)

Authors: Matthieu Sozeau (Inria & LS2N, Université de Nantes)

Comments: In Proceedings LFMTP 2021, arXiv:2107.07376

Journal-ref: EPTCS 337, 2021, pp. 13-29

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

[104]  arXiv:2107.09119 (cross-list from cs.MA) [pdf, ps, other]

Title: Rational Verification for Probabilistic Systems

Authors: Julian Gutierrez, Lewis Hammond, Anthony W. Lin, Muhammad Najib, Michael Wooldridge

Comments: 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021)

Subjects: Multiagent Systems (cs.MA); Artificial Intelligence (cs.AI); Computer Science and Game Theory (cs.GT); Logic in Computer Science (cs.LO)

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

Title: QRAT Polynomially Simulates Merge Resolution

Authors: Sravanthi Chede, Anil Shukla

Comments: 12 pages, 1 figure

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

[106]  arXiv:2107.09423 (cross-list from cs.CC) [pdf, ps, other]

Title: Combinatorial Gap Theorem and Reductions between Promise CSPs

Authors: Libor Barto, Marcin Kozik

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

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

Title: Answer-Set Programs for Reasoning about Counterfactual Interventions and Responsibility Scores for Classification

Authors: Leopoldo Bertossi, Gabriela Reyes

Comments: Revised for camera ready. Extended version with appendices of paper to appear in IJCLR'21. arXiv admin note: text overlap with arXiv:2106.10562

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

[108]  arXiv:2107.10160 (cross-list from cs.PL) [pdf, ps, other]

Title: Pre-proceedings of the 31st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021)

Authors: Emanuele De Angelis, Wim Vanhoof

Comments: Papers selected for presentation at LOPSTR 2021, Invited talks and Tutorial

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

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

Title: Abstract Reasoning via Logic-guided Generation

Authors: Sihyun Yu, Sangwoo Mo, Sungsoo Ahn, Jinwoo Shin

Comments: ICML 2021 Workshop on Self-Supervised Learning for Reasoning and Perception (Spotlight Talk)

Subjects: Machine Learning (cs.LG); Artificial Intelligence (cs.AI); Computer Vision and Pattern Recognition (cs.CV); Logic in Computer Science (cs.LO)

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

Title: Lower Bounds for Symmetric Circuits for the Determinant

Authors: Anuj Dawar, Gregory Wilsenach

Comments: 29 Pages

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

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

Title: Neural Circuit Synthesis from Specification Patterns

Authors: Frederik Schmitt, Christopher Hahn, Markus N. Rabe, Bernd Finkbeiner

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

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

Title: Logics Meet 2-Way 1-Clock Alternating Timed Automata

Authors: Shankara Narayanan Krishna, Khushraj Nanik Madnani, Manuel Mazo Jr., Paritosh K. Pandya

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

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

[113]  arXiv:2107.13827 (cross-list from cs.ET) [pdf, other]

Title: ReCo1: A Fault resilient technique of Correlation Sensitive Stochastic Designs

Authors: Shyamali Mitra, Sayantan Banerjee, Mrinal Kanti Naskar

Comments: 24 pages,20 figures, 2 tables, 3 algorithms

Subjects: Emerging Technologies (cs.ET); Logic in Computer Science (cs.LO)

[114]  arXiv:2107.14325 (cross-list from cs.CR) [pdf, ps, other]

Title: PiBase: An IoT-based Security System using Raspberry Pi and Google Firebase

Authors: Venkat Margapuri, Niketa Penumajji, Mitchell Neilsen

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

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

Title: On Strong Observational Refinement and Forward Simulation

Authors: John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Comments: Full version of the paper to appear in DISC 2021

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

[116]  arXiv:2107.00108 (cross-list from math.OC) [pdf, other]

Title: Convex Optimization for Parameter Synthesis in MDPs

Authors: Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu

Comments: Submitted to IEEE TAC

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

[117]  arXiv:2107.01186 (cross-list from quant-ph) [pdf, ps, other]

Title: Quantum Multiple-Valued Decision Diagrams in Graphical Calculi

Authors: Renaud Vilmart

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

[118]  arXiv:2107.08324 (cross-list from quant-ph) [pdf, ps, other]

Title: Quantum circuits with classical channels and the principle of deferred measurements

Authors: Yuri Gurevich, Andreas Blass

Subjects: Quantum Physics (quant-ph); Information Theory (cs.IT); Logic in Computer Science (cs.LO); Mathematical Physics (math-ph)

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

Title: Dynamic Cantor Derivative Logic

Authors: David Fernández-Duque, Yoàv Montacute

Comments: Extended version of the paper in Computer Science Logic (CSL) 2022 Proceedings

Journal-ref: Logical Methods in Computer Science, Volume 19, Issue 4 (December 18, 2023) lmcs:10042

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

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

Title: Specifying a Game-Theoretic Extensive Form as an Abstract 5-ary Relation

Authors: Peter A. Streufert

Comments: 57 pages, 10 figures. Version 3 (February 7) is extensively rewritten, with new tools and applications. Version 4 (February 10) updates cross-references. [Version 1 is Western University Department of Economics Research Report 2021-3.]

Subjects: Theoretical Economics (econ.TH); Computer Science and Game Theory (cs.GT); Logic in Computer Science (cs.LO); Optimization and Control (math.OC)

[121]  arXiv:2107.12144 (cross-list from quant-ph) [pdf, ps, other]

Title: Quantum Information Effects

Authors: Chris Heunen, Robin Kaarsgaard

Comments: 27 pages, accepted for POPL 2022

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

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

Title: Cosine and Computation

Authors: Prabhat Kumar Jha

Comments: Submitted to FSTTCS 2021

Subjects: Logic (math.LO); Discrete Mathematics (cs.DM); Logic in Computer Science (cs.LO); Number Theory (math.NT)

[123]  arXiv:2107.14031 (cross-list from math.CT) [pdf, ps, other]

Title: Doctrines, modalities and comonads

Authors: Francesco Dagnino, Giuseppe Rosolini

Journal-ref: Math. Struct. Comp. Sci. 31 (2021) 769-798

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

[124]  arXiv:2107.14581 (cross-list from quant-ph) [pdf, ps, other]

Title: Causality in Higher Order Process Theories

Authors: Matt Wilson, Giulio Chiribella

Comments: In Proceedings QPL 2021, arXiv:2109.04886

Journal-ref: EPTCS 343, 2021, pp. 265-300

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