Logic in Computer Science

Authors and titles for February 2019

[51] arXiv:1902.08420 [pdf, other]

Title: Automating the Diagram Method to Prove Correctness of Program Transformations

David Sabel (Goethe-University Frankfurt am Main)

Comments: In Proceedings WPTE 2018, arXiv:1902.07818

Journal-ref: EPTCS 289, 2019, pp. 17-33

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

[52] arXiv:1902.08421 [pdf, other]

Title: On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems

Yoshiaki Kanazawa (Nagoya University), Naoki Nishida (Nagoya University)

Comments: In Proceedings WPTE 2018, arXiv:1902.07818

Journal-ref: EPTCS 289, 2019, pp. 34-52

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

[53] arXiv:1902.08423 [pdf, other]

Title: On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions

Naoki Nishida (Nagoya University), Yuya Maeda (Nagoya University)

Comments: In Proceedings WPTE 2018, arXiv:1902.07818

Journal-ref: EPTCS 289, 2019, pp. 68-87

Subjects: Logic in Computer Science (cs.LO)

[54] arXiv:1902.08765 [pdf, other]

Title: Fully Automatic, Verified Classification of all Frankl-Complete (FC(6)) Set Families

Filip Marić, Bojan Vučković, Miodrag Živković

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

[55] arXiv:1902.08789 [pdf, other]

Title: Experimental Study on CTL model checking using Machine Learning

Weijun ZHU

Comments: 5 pages, 1 figure

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

[56] arXiv:1902.08847 [pdf, other]

Title: Automated proof search system for logic of correlated knowledge

Haroldas Giedra, Romas Alonderis

Subjects: Logic in Computer Science (cs.LO)

[57] arXiv:1902.08848 [pdf, other]

Title: Algebraic Type Theory and Universe Hierarchies

Jonathan Sterling

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

[58] arXiv:1902.09214 [pdf, other]

Title: Homogenousness and Specificity

Karl Schlechta

Subjects: Logic in Computer Science (cs.LO)

[59] arXiv:1902.09539 [pdf, other]

Title: Dependent choice as a termination principle

Thomas Powell

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

[60] arXiv:1902.09693 [pdf, other]

Title: A New Linear Time Correctness Condition for Multiplicative Linear Logic

Satoshi Matsuoka

Comments: Found an bug in the proof of the linear time claim in the second version. Adapted the algorithm in order to guarantee the linear time termination. Added an additional example

Subjects: Logic in Computer Science (cs.LO)

[61] arXiv:1902.09844 [pdf, other]

Title: Adding the Power-Set to Description Logics

Laura Giordano, Alberto Policriti

Comments: 30 pages

Journal-ref: Theoretical Computer Science, November 2019

Subjects: Logic in Computer Science (cs.LO)

[62] arXiv:1902.09880 [pdf, other]

Title: Correct and Efficient Antichain Algorithms for Refinement Checking

Maurice Laveaux, Jan Friso Groote, Tim A.C. Willemse

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

Subjects: Logic in Computer Science (cs.LO)

[63] arXiv:1902.09900 [pdf, other]

Title: SLD-Resolution Reduction of Second-Order Horn Fragments -- technical report --

Sophie Tourret, Andrew Cropper

Comments: technical report, extends a conference paper accepted at JELIA 2019 with detailed proofs

Subjects: Logic in Computer Science (cs.LO)

[64] arXiv:1902.10396 [pdf, other]

Title: HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories

C.-H. Luke Ong, Dominik Wagner

Subjects: Logic in Computer Science (cs.LO)

[65] arXiv:1902.10452 [pdf, other]

Title: Algebraic Invariants for Linear Hybrid Automata

Rupak Majumdar, Joël Ouaknine, Amaury Pouly, James Worrell

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

[66] arXiv:1902.10820 [pdf, other]

Title: From Cubes to Twisted Cubes via Graph Morphisms in Type Theory

Gun Pinyo, Nicolai Kraus

Comments: v4: 18 pages, postproceedings of TYPES'2019

Subjects: Logic in Computer Science (cs.LO)

[67] arXiv:1902.10971 [pdf, other]

Title: Representing Continuous Functions between Greatest Fixed Points of Indexed Containers

Pierre Hyvernat

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

Subjects: Logic in Computer Science (cs.LO)

[68] arXiv:1902.11189 [pdf, other]

Title: Semantics of higher-order probabilistic programs with conditioning

Fredrik Dahlqvist, Dexter Kozen

Comments: 17 pages, proofs in the Appendix

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

[69] arXiv:1902.11263 [pdf, other]

Title: Sequentiality of String-to-Context Transducers

Pierre-Alain Reynier, Didier Villevalois

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

[70] arXiv:1902.00325 (cross-list from quant-ph) [pdf, other]

Title: Quantum Hoare Logic with Ghost Variables

Dominique Unruh

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

[71] arXiv:1902.00343 (cross-list from quant-ph) [pdf, other]

Title: Categorical Operational Physics

Sean Tull

Comments: DPhil Thesis, University of Oxford

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

[72] arXiv:1902.02333 (cross-list from math.CO) [pdf, other]

Title: Unary Patterns of Size Four with Morphic Permutations

Kamellia Reshadi

Comments: Accepted in the Student Research Forum (SRF) of SOFSEM 2019 conference

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

[73] arXiv:1902.03178 (cross-list from quant-ph) [pdf, other]

Title: Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus

Ross Duncan, Aleks Kissinger, Simon Perdrix, John van de Wetering

Comments: 18 pages + appendices with examples, proofs, and pseudocode

Journal-ref: Quantum 4, 279 (2020)

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

[74] arXiv:1902.03218 (cross-list from quant-ph) [pdf, other]

Title: Model Checking Applied to Quantum Physics

Ji Guan, Yuan Feng, Andrea Turrini, Mingsheng Ying

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

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

Title: Learning Ontologies with Epistemic Reasoning: The EL Case

Ana Ozaki, Nicolas Troquard

Comments: Technical report

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

[76] arXiv:1902.03431 (cross-list from math.CO) [pdf, other]

Title: On the maximal minimal cube lengths in distinct DNF tautologies

Manuel Kauers, Martina Seidl, Doron Zeilberger

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

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

Title: Security-Aware Synthesis Using Delayed-Action Games

Mahmoud Elfar, Yu Wang, Miroslav Pajic

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

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

Title: Program Equivalence for Algebraic Effects via Modalities

Cristina Matache

Comments: Master Thesis, University of Oxford (September 2018)

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

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

Title: CSPs with Global Modular Constraints: Algorithms and Hardness via Polynomial Representations

Joshua Brakensiek, Sivakanth Gopi, Venkatesan Guruswami

Comments: 52 pages; to appear in STOC 2019

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

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

Title: HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification

Luis Garcia, Stefan Mitsch, Andre Platzer

Comments: 13 pages, 9 figures. ICCPS 2019

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

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

Title: Overt choice

Matthew de Brecht, Arno Pauly, Matthias Schröder

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

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

Title: Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus

Andreas Abel, Christian Sattler

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

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

Title: Canonicity and homotopy canonicity for cubical type theory

Thierry Coquand, Simon Huber, Christian Sattler

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

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

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

Title: Continuous Ordinary Differential Equations and Transfinite Computations

Olivier Bournez, Sabrina Ouazzani

Comments: The model is not sufficiently precisely detailed. Part of the article needs clarification and rewriting

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

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

Title: The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space

Yannick Forster, Fabian Kunze, Marc Roth

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

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

Title: Aperiodic Weighted Automata and Weighted First-Order Logic

Manfred Droste, Paul Gastin

Comments: An extended abstract of the paper appeared at MFCS'19

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

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

Title: Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification

Jianlin Li, Pengfei Yang, Jiangchao Liu, Liqian Chen, Xiaowei Huang, Lijun Zhang

Comments: SAS 2019: 26th Static Analysis Symposium, Porto, Portugal, October 8-11, 2019

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

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

Title: The Cpi-calculus: a Model for Confidential Name Passing

Ivan Prokić (Faculty of Technical Sciences, University of Novi Sad, Serbia)

Comments: In Proceedings ICE 2019, arXiv:1909.05242

Journal-ref: EPTCS 304, 2019, pp. 115-136

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

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

Title: A conformance relation and complete test suites for I/O systems

Adilson Luiz Bonifacio, Arnaldo Vieira Moura

Comments: 44 pages, 20 figures

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