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)