Logic in Computer Science

Authors and titles for February 2012

[1] arXiv:1202.0904 [pdf, other]

Title: Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)

Murdoch Gabbay, Aleksandar Nanevski

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

[2] arXiv:1202.0914 [pdf, other]

Title: Type-elimination-based reasoning for the description logic SHIQbs using decision diagrams and disjunctive datalog

Sebastian Rudolph (Karlsruhe Institute of Technology), Markus Krötzsch (Oxford University), Pascal Hitzler (Wright State University, Dayton, Ohio)

Comments: 38 pages, 3 figures, camera ready version of paper accepted for publication in Logical Methods in Computer Science

Journal-ref: Logical Methods in Computer Science, Volume 8, Issue 1 (February 27, 2012) lmcs:806

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

[3] arXiv:1202.1309 [pdf, other]

Title: A Decidable Fragment of Strategy Logic

Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi

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

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

[4] arXiv:1202.1641 [pdf, other]

Title: On the Invariance of the Unitary Cost Model for Head Reduction (Long Version)

Beniamino Accattoli, Ugo Dal Lago

Comments: 22 pages

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

[5] arXiv:1202.1980 [pdf, other]

Title: First-Order Logic on Higher-Order Nested Pushdown Trees

Alexander Kartzow

Comments: 41 pages

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

[6] arXiv:1202.2296 [pdf, other]

Title: An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning

Maria Luisa Bonet, Sam Buss

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

[7] arXiv:1202.2407 [pdf, other]

Title: Proceedings Fourth Workshop on Mathematically Structured Functional Programming

James Chapman (Institute of Cybernetics, Tallinn), Paul Blain Levy (University of Birmingham)

Journal-ref: EPTCS 76, 2012

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

[8] arXiv:1202.3174 [pdf, other]

Title: Proceedings 8th Workshop on Fixed Points in Computer Science

Dale Miller (INRIA-Saclay, France), Zoltán Ésik (University of Szeged, Hungary)

Comments: For more information about FICS 2012, please visit the webpage of the conference: this http URL

Journal-ref: EPTCS 77, 2012

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

[9] arXiv:1202.3264 [pdf, other]

Title: Generalized powerlocales via relation lifting

Yde Venema, Steve Vickers, Jacob Vosmaer

Comments: 44 pages

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

[10] arXiv:1202.3317 [pdf, other]

Title: An Higher-Order Characterization of Probabilistic Polynomial Time (Long Version)

Ugo Dal Lago, Paolo Parisen Toldin

Comments: 32 pages

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

[11] arXiv:1202.3484 [pdf, other]

Title: Symbolic bisimulation for quantum processes

Yuan Feng, Yuxin Deng, Mingsheng Ying

Comments: 30 pages, 7 figures, comments are welcome

Subjects: Logic in Computer Science (cs.LO)

[12] arXiv:1202.3496 [pdf, other]

Title: Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types

Andreas Abel (Department of Computer Science, Ludwig-Maximilians-University Munich)

Comments: In Proceedings FICS 2012, arXiv:1202.3174

Journal-ref: EPTCS 77, 2012, pp. 1-11

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

[13] arXiv:1202.3497 [pdf, other]

Title: Characteristic Formulae for Relations with Nested Fixed Points

Luca Aceto, Anna Ingólfsdóttir

Comments: In Proceedings FICS 2012, arXiv:1202.3174

Journal-ref: EPTCS 77, 2012, pp. 15-22

Subjects: Logic in Computer Science (cs.LO)

[14] arXiv:1202.3498 [pdf, other]

Title: IO vs OI in Higher-Order Recursion Schemes

Axel Haddad (LIGM & LIAFA)

Comments: In Proceedings FICS 2012, arXiv:1202.3174

Journal-ref: EPTCS 77, 2012, pp. 23-30

Subjects: Logic in Computer Science (cs.LO)

[15] arXiv:1202.3500 [pdf, other]

Title: Model-Checking the Higher-Dimensional Modal mu-Calculus

Martin Lange (School of Electrical Engineering and Computer Science, University of Kassel, Germany), Etienne Lozes (School of Electrical Engineering and Computer Science, University of Kassel, Germany)

Comments: In Proceedings FICS 2012, arXiv:1202.3174

Journal-ref: EPTCS 77, 2012, pp. 39-46

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

[16] arXiv:1202.3501 [pdf, other]

Title: Cut-elimination for the mu-calculus with one variable

Grigori Mints, Thomas Studer

Comments: In Proceedings FICS 2012, arXiv:1202.3174

Journal-ref: EPTCS 77, 2012, pp. 47-54

Subjects: Logic in Computer Science (cs.LO)

[17] arXiv:1202.3502 [pdf, other]

Title: Structured general corecursion and coinductive graphs [extended abstract]

Tarmo Uustalu

Comments: In Proceedings FICS 2012, arXiv:1202.3174

Journal-ref: EPTCS 77, 2012, pp. 55-61

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

[18] arXiv:1202.3538 [pdf, other]

Title: Refinement Modal Logic

Laura Bozzelli, Hans van Ditmarsch, Tim French, James Hales, Sophie Pinchinat

Journal-ref: Information and Computation, Volume 239, December 2014, Pages 303-339

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

[19] arXiv:1202.4144 [pdf, other]

Title: Towards an efficient prover for the C1 paraconsistent logic

Adolfo Neto, Celso A. A. Kaestner, Marcelo Finger

Comments: 16 pages

Journal-ref: Electronic Notes in Theoretical Computer Science. Volume 256, 2 December 2009, Pages 87-102. Proceedings of the Fourth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2009)

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

[20] arXiv:1202.4175 [pdf, other]

Title: Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives

Krishnendu Chatterjee, Manas Joglekar, Nisarg Shah

Subjects: Logic in Computer Science (cs.LO)

[21] arXiv:1202.4193 [pdf, other]

Title: Exponential Lower Bounds and Separation for Query Rewriting

Stanislav Kikot, Roman Kontchakov, Vladimir Podolskii, Michael Zakharyaschev

Subjects: Logic in Computer Science (cs.LO)

[22] arXiv:1202.4281 [pdf, other]

Title: Bounded Termination of Monotonicity-Constraint Transition Systems

Amir M. Ben-Amram, Michael Vainer

Comments: 46 pages. Research has been presented at DICE 2011 (Saarbruecken, Germany, March 2011), 2FC 2011 (Novi Sad, Serbia, May 2011) and DANSAS (Odense, Denmark, August 2011). Revised (twice) to correct errors in previous versions

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

[23] arXiv:1202.4509 [pdf, other]

Title: Rich Counter-Examples for Temporal-Epistemic Logic Model Checking

Simon Busard (UCLouvain, Belgium), Charles Pecheur (UCLouvain, Belgium)

Comments: In Proceedings IWIGP 2012, arXiv:1202.4229

Journal-ref: EPTCS 78, 2012, pp. 39-53

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

[24] arXiv:1202.4678 [pdf, other]

Title: A Categorical Model for the Lambda Calculus with Constructors

Barbara Petit

Comments: 21 pages

Subjects: Logic in Computer Science (cs.LO)

[25] arXiv:1202.4824 [pdf, other]

Title: A General Form of Attribute Exploration

Daniel Borchmann

Subjects: Logic in Computer Science (cs.LO)

[26] arXiv:1202.4829 [pdf, other]

Title: An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support

Ralph-Johan Back (Åbo Akademi University), Johannes Eriksson (Åbo Akademi University)

Comments: In Proceedings THedu'11, arXiv:1202.4535

Journal-ref: EPTCS 79, 2012, pp. 29-48

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

[27] arXiv:1202.4832 [pdf, other]

Title: Automated Generation of User Guidance by Combining Computation and Deduction

Walther Neuper

Comments: In Proceedings THedu'11, arXiv:1202.4535

Journal-ref: EPTCS 79, 2012, pp. 82-101

Subjects: Logic in Computer Science (cs.LO); Human-Computer Interaction (cs.HC); Programming Languages (cs.PL)

[28] arXiv:1202.4834 [pdf, other]

Title: Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs

Wolfgang Schreiner

Comments: In Proceedings THedu'11, arXiv:1202.4535

Journal-ref: EPTCS 79, 2012, pp. 124-142

Subjects: Logic in Computer Science (cs.LO); Mathematical Software (cs.MS); Programming Languages (cs.PL); Symbolic Computation (cs.SC)

[29] arXiv:1202.4835 [pdf, other]

Title: Isabelle/PIDE as Platform for Educational Tools

Makarius Wenzel, Burkhart Wolff

Comments: In Proceedings THedu'11, arXiv:1202.4535

Journal-ref: EPTCS 79, 2012, pp. 143-153

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

[30] arXiv:1202.4905 [pdf, other]

Title: A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions

Andrea Asperti (University of Bologna), Wilmer Ricciotti (University of Bologna), Claudio Sacerdoti Coen (University of Bologna), Enrico Tassi (INRIA - Microsoft Research)

Journal-ref: Logical Methods in Computer Science, Volume 8, Issue 1 (March 2, 2012) lmcs:1044

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

[31] arXiv:1202.5850 [pdf, other]

Title: The Cost of Parameterized Reachability in Mobile Ad Hoc Networks

Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso, Gianluigi Zavattaro

Subjects: Logic in Computer Science (cs.LO)

[32] arXiv:1202.6148 [pdf, other]

Title: Instance Based Methods --- A Brief Overview

Peter Baumgartner, Evgenij Thorstensen

Comments: Final publication availible at this http URL

Journal-ref: KI - K\"unstliche Intelligenz 24(1):35--42, 2010

Subjects: Logic in Computer Science (cs.LO)

[33] arXiv:1202.6352 [pdf, other]

Title: Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability

Matthias Baaz (Department of Discrete Mathematics and Geometry, TU Vienna), Agata Ciabattoni (Department of Computer Languages, TU Vienna), Christian G Fermüller (Department of Computer Languages, TU Vienna)

Comments: 23 pages, accepted for LMCS (Logical Methods in Computer Science)

Journal-ref: Logical Methods in Computer Science, Volume 8, Issue 1 (March 6, 2012) lmcs:833

Subjects: Logic in Computer Science (cs.LO)

[34] arXiv:1202.6472 [pdf, other]

Title: First steps towards the certification of an ARM simulator using Compcert

Xiaomu Shi (LIAMA), Jean-François Monin (LIAMA, UJF), Frederic Tuong (LIAMA), Frédéric Blanqui (LIAMA)

Comments: First International Conference on Certified Programs and Proofs 7086 (2011)

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

[35] arXiv:1202.6473 [pdf, other]

Title: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

Frédéric Blanqui (LIAMA), Adam Koprowski

Journal-ref: Mathematical Structures in Computer Science 21, 4 (2011) 827-859

Subjects: Logic in Computer Science (cs.LO)

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

Title: First-Order Model Checking on Generalisations of Pushdown Graphs

Alexander Kartzow

Comments: phd thesis, 255 pages

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

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

Title: Relational Semantics for Databases and Predicate Calculus

Philip Kelly, M. H. van Emden

Comments: 18 pages, 8 figures. arXiv admin note: text overlap with arXiv:cs/0607039

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

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

Title: From heaps of matches to the limits of computability

Urban Larsson, Johan Wästlund

Comments: 13 pages, 7 figures

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

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

Title: On a coalgebraic view on Logic

Dirk Hofmann, Manuel A. Martins

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

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

Title: Optimization in SMT with LA(Q) Cost Functions

Roberto Sebastiani, Silvia Tomasi

Comments: A shorter version is currently under submission

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

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

Title: Step-Indexed Normalization for a Language with General Recursion

Chris Casinghino (University of Pennsylvania), Vilhelm Sjöberg (University of Pennsylvania), Stephanie Weirich (University of Pennsylvania)

Comments: In Proceedings MSFP 2012, arXiv:1202.2407

Journal-ref: EPTCS 76, 2012, pp. 25-39

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

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

Title: Lattices of Logical Fragments over Words

Manfred Kufleitner, Alexander Lauser

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

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

Title: Initial Semantics for Strengthened Signatures

André Hirschowitz (Laboratoire J.-A. Dieudonné, Université de Nice - Sophia Antipolis), Marco Maggesi (Dipartimento di Matematica "U. Dini", Università degli Studi di Firenze)

Comments: In Proceedings FICS 2012, arXiv:1202.3174

Journal-ref: EPTCS 77, 2012, pp. 31-38

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

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

Title: Higher-order illative combinatory logic

Łukasz Czajka

Journal-ref: Journal of Symbolic Logic, vol. 78, issue 3, pp. 837-872, 2013

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

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

Title: Alternating register automata on finite words and trees

Diego Figueira (INRIA & ENS Cachan, LSV)

Journal-ref: Logical Methods in Computer Science, Volume 8, Issue 1 (March 9, 2012) lmcs:907

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

[46] arXiv:1202.4535 (cross-list from cs.SY) [pdf, other]

Title: Proceedings First Workshop on CTP Components for Educational Software

Pedro Quaresma (University of Coimbra, Portugal), Ralph-Johan Back (Åbo Akademi University, Finland)

Journal-ref: EPTCS 79, 2012

Subjects: Systems and Control (eess.SY); Logic in Computer Science (cs.LO); Mathematical Software (cs.MS); Symbolic Computation (cs.SC)

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

Title: Towards an Intelligent Tutor for Mathematical Proofs

Serge Autexier (German Research Center for Artificial Intelligence (DFKI), Bremen, Germany), Dominik Dietrich (German Research Center for Artificial Intelligence (DFKI), Bremen, Germany), Marvin Schiller (Brunel University, London, UK)

Comments: In Proceedings THedu'11, arXiv:1202.4535

Journal-ref: EPTCS 79, 2012, pp. 1-28

Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Mathematical Software (cs.MS); Symbolic Computation (cs.SC)

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

Title: Formalization and Implementation of Algebraic Methods in Geometry

Filip Marić (Faculty of Mathematics, University of Belgrade, Serbia), Ivan Petrović (Faculty of Mathematics, University of Belgrade, Serbia), Danijela Petrović (Faculty of Mathematics, University of Belgrade, Serbia), Predrag Janičić (Faculty of Mathematics, University of Belgrade, Serbia)

Comments: In Proceedings THedu'11, arXiv:1202.4535

Journal-ref: EPTCS 79, 2012, pp. 63-81

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

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

Title: Bare canonicity of representable cylindric and polyadic algebras

Jannis Bulian, Ian Hodkinson

Journal-ref: Annals of Pure and Applied Logic 164 (2013), pp. 884-906

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