Logic in Computer Science

Authors and titles for cs.LO in Jun 2014

[1]  arXiv:1406.0043 [pdf, other]

Title: SAT Modulo Monotonic Theories

Authors: Sam Bayless, Noah Bayless, Holger H. Hoos, Alan J. Hu

Subjects: Logic in Computer Science (cs.LO)

[2]  arXiv:1406.0303 [pdf, other]

Title: A Superposition Calculus for Abductive Reasoning

Authors: Mnacho Echenim, Nicolas Peltier

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

[3]  arXiv:1406.0349 [pdf, ps, other]

Title: Undecidability of satisfiability in the algebra of finite binary relations with union, composition, and difference

Authors: Tony Tan, Jan Van den Bussche, Xiaowang Zhang

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

[4]  arXiv:1406.0774 [pdf, other]

Title: Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?

Authors: Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat

Comments: Preprint of a paper accepted for the forthcoming CICM 2014 conference (cicm-conference.org/2014): S.M. Watt et al. (Eds.): CICM 2014, LNAI 8543, Springer International Publishing Switzerland 2014. 16 pages, 1 figure

Subjects: Logic in Computer Science (cs.LO)

[5]  arXiv:1406.0893 [pdf, ps, other]

Title: Query Answering over Contextualized RDF/OWL Knowledge with Forall-Existential Bridge Rules: Attaining Decidability using Acyclicity (full version)

Authors: Mathew Joseph, Gabriel Kuper, Luciano Serafini

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

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

Title: Petri Games: Synthesis of Distributed Systems with Causal Memory

Authors: Bernd Finkbeiner (Universität des Saarlandes), Ernst-Rüdiger Olderog (Carl von Ossietzky Universität Oldenburg)

Comments: In Proceedings GandALF 2014, arXiv:1408.5560

Journal-ref: EPTCS 161, 2014, pp. 217-230

Subjects: Logic in Computer Science (cs.LO)

[7]  arXiv:1406.1238 [pdf, ps, other]

Title: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications

Authors: Freek Verbeek (Open University of The Netherlands), Julien Schmaltz (Eindhoven University of Technology)

Journal-ref: EPTCS 152, 2014

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

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

Title: Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi

Authors: Benoît Valiron, Steve Zdancewic

Comments: Accepted at ICTAC 2014. The final publication will be available at link.springer.com

Journal-ref: Proc. of ICTAC'14, in LNCS vol. 8687, pp 442-459 (2014)

Subjects: Logic in Computer Science (cs.LO)

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

Title: Polymorphic Types in ACL2

Authors: Benjamin Selfridge (University of Texas at Austin), Eric Smith (Kestrel Institute)

Comments: In Proceedings ACL2 2014, arXiv:1406.1238

Journal-ref: EPTCS 152, 2014, pp. 49-59

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

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

Title: Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis

Authors: John Cowles (University of Wyoming), Ruben Gamboa (University of Wyoming)

Comments: In Proceedings ACL2 2014, arXiv:1406.1238

Journal-ref: EPTCS 152, 2014, pp. 89-100

Subjects: Logic in Computer Science (cs.LO)

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

Title: Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent

Authors: Ruben Gamboa (University of Wyoming), John Cowles (University of Wyoming)

Comments: In Proceedings ACL2 2014, arXiv:1406.1238

Journal-ref: EPTCS 152, 2014, pp. 101-110

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

[12]  arXiv:1406.1562 [pdf, other]

Title: Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis

Authors: Disha Puri (Dept. of Computer Science, Portland State University), Sandip Ray (Strategic CAD Labs, Intel Corporation), Kecheng Hao (Dept. of Computer Science, Portland State University), Fei Xie (Dept. of Computer Science, Portland State University)

Comments: In Proceedings ACL2 2014, arXiv:1406.1238

Journal-ref: EPTCS 152, 2014, pp. 111-128

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

[13]  arXiv:1406.1563 [pdf, ps, other]

Title: An ACL2 Mechanization of an Axiomatic Framework for Weak Memory

Authors: Benjamin Selfridge (University of Texas at Austin)

Comments: In Proceedings ACL2 2014, arXiv:1406.1238

Journal-ref: EPTCS 152, 2014, pp. 129-144

Subjects: Logic in Computer Science (cs.LO)

[14]  arXiv:1406.1567 [pdf, ps, other]

Title: Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems

Authors: Nathalie Bertrand (INRIA, Rennes), Luca Bortolussi (University of Trieste)

Journal-ref: EPTCS 154, 2014

Subjects: Logic in Computer Science (cs.LO); Computational Engineering, Finance, and Science (cs.CE); Performance (cs.PF)

[15]  arXiv:1406.1633 [pdf, ps, other]

Title: The dagger lambda calculus

Authors: Philip Atzemoglou (University of Oxford)

Comments: In Proceedings QPL 2014, arXiv:1412.8102

Journal-ref: EPTCS 172, 2014, pp. 217-235

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

[16]  arXiv:1406.1920 [pdf, other]

Title: Probabilistic bounded reachability for hybrid systems with continuous nondeterministic and probabilistic parameters

Authors: Fedor Shmarov, Paolo Zuliani

Subjects: Logic in Computer Science (cs.LO)

[17]  arXiv:1406.1965 [pdf, ps, other]

Title: An Algebraic Characterisation of Concurrent Composition

Authors: Samson Abramsky

Comments: This is an old technical report from 1981. I submitted it to a special issue of HOSC in honour of Peter Landin, as explained in the Prelude, added in 2008. However, at an advanced stage, the handling editor became unresponsive, and the paper was never published. I am making it available via the arXiv for the same reasons given in the Prelude

Subjects: Logic in Computer Science (cs.LO)

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

Title: Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types

Authors: Andreas Abel (Gothenburg University), James Chapman (Institute of Cybernetics, Tallinn)

Comments: In Proceedings MSFP 2014, arXiv:1406.1534

Journal-ref: EPTCS 153, 2014, pp. 51-67

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

[19]  arXiv:1406.2064 [pdf, other]

Title: Coherence for Skew-Monoidal Categories

Authors: Tarmo Uustalu

Comments: In Proceedings MSFP 2014, arXiv:1406.1534

Journal-ref: EPTCS 153, 2014, pp. 68-77

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

[20]  arXiv:1406.2066 [pdf, other]

Title: GSOS for non-deterministic processes with quantitative aspects

Authors: Marino Miculan (DiMI, University of Udine), Marco Peressotti (DiMI, University of Udine)

Comments: In Proceedings QAPL 2014, arXiv:1406.1567

Journal-ref: EPTCS 154, 2014, pp. 17-33

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

[21]  arXiv:1406.2068 [pdf, other]

Title: MeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata

Authors: Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger Hermanns

Comments: In Proceedings QAPL 2014, arXiv:1406.1567

Journal-ref: EPTCS 154, 2014, pp. 48-63

Subjects: Logic in Computer Science (cs.LO)

[22]  arXiv:1406.2079 [pdf, ps, other]

Title: Program Verification of Numerical Computation - Part 2

Authors: Garry Pantelis

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

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

[23]  arXiv:1406.2103 [pdf, ps, other]

Title: A composable language for action models

Authors: Tim French, James Hales, Edwin Tay

Comments: Extended version of a paper to appear in the 10th International Conference on Advances in Modal Logic (AiML)

Subjects: Logic in Computer Science (cs.LO)

[24]  arXiv:1406.2110 [pdf, other]

Title: Logic Programming and Logarithmic Space

Authors: Clément Aubert, Marc Bagnol, Paolo Pistone, Thomas Seiller

Subjects: Logic in Computer Science (cs.LO)

[25]  arXiv:1406.2161 [pdf, ps, other]

Title: Tableaux for Dynamic Logic of Propositional Assignments

Authors: Tiago de Lima, Andreas Herzig

Comments: 20 pages

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