Logic in Computer Science

Authors and titles for February 2012

[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)