Logic for Programming, Artificial Intelligence, and Reasoning

1. Front Matter

   PDF

2. The TPTP World – Infrastructure for Automated Reasoning

   • Geoff Sutcliffe

   Pages 1-12

3. Speed-Up Techniques for Negation in Grounding

   • Amir Aavani, Shahab Tasharrofi, Gulay Unel, Eugenia Ternovska, David Mitchell

   Pages 13-26

4. Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation

   • Gourinath Banda, John P. Gallagher

   Pages 27-45

5. On the Equality of Probabilistic Terms

   • Gilles Barthe, Marion Daubignard, Bruce Kapron, Yassine Lakhnech, Vincent Laporte

   Pages 46-63

6. Program Logics for Homogeneous Meta-programming

   • Martin Berger, Laurence Tratt

   Pages 64-81

7. Verifying Pointer and String Analyses with Region Type Systems

   • Lennart Beringer, Robert Grabowski, Martin Hofmann

   Pages 82-102

8. ABC: Algebraic Bound Computation for Loops

   • Régis Blanc, Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács

   Pages 103-118

9. Hardness of Preorder Checking for Basic Formalisms

   • Laura Bozzelli, Axel Legay, Sophie Pinchinat

   Pages 119-135

10. A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae

    • Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, Michel Parigot

    Pages 136-153

11. Pairwise Cardinality Networks

    • Michael Codish, Moshe Zazon-Ivry

    Pages 154-172

12. Logic and Computation in a Lambda Calculus with Intersection and Union Types

    • Daniel J. Dougherty, Luigi Liquori

    Pages 173-191

13. Graded Alternating-Time Temporal Logic

    • Marco Faella, Margherita Napoli, Mimmo Parente

    Pages 192-211

14. Non-oblivious Strategy Improvement

    • John Fearnley

    Pages 212-230

15. A Simple Class of Kripke-Style Models in Which Logic and Computation Have Equal Standing

    • Michael Gabbay, Murdoch J. Gabbay

    Pages 231-254

16. Label-Free Proof Systems for Intuitionistic Modal Logic IS5

    • Didier Galmiche, Yakoub Salhi

    Pages 255-271

17. An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory

    • Yoichi Hirai

    Pages 272-289

18. Disunification for Ultimately Periodic Interpretations

    • Matthias Horbach

    Pages 290-311

19. Synthesis of Trigger Properties

    • Orna Kupferman, Moshe Y. Vardi

    Pages 312-331

20. Semiring-Induced Propositional Logic: Definition and Basic Algorithms

    • Javier Larrosa, Albert Oliveras, Enric Rodríguez-Carbonell

    Pages 332-347

This book constitutes the thoroughly refereed post-conference proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010, which took place in Dakar, Senegal, in April/May 2010. The 27 revised full papers and 9 revised short papers presented together with 1 invited talk were carefully revised and selected from 47 submissions. The papers address all current issues in automated reasoning, computational logic, programming languages and deal with logic programming, logic-based program manipulation, formal methods, and various kinds of AI logics. Subjects covered range from theoretical aspects to various applications such as automata, linear arithmetic, verification, knowledge representation, proof theory, quantified constraints, as well as modal and temporal logics.

• AI logics
• DPLL
• SAT solvers
• SMT solving
• abstraction
• automata theory
• automated deduction
• automated reasoning
• constraints
• description logics
• distributed systems
• formal verification
• logic programming
• marginalization problem
• matrix interpretations
• model checking
• non-linear arithmetic
• normalization
• propositional logic
• query automata
• reduction systems
• resolution
• satisfiability
• semiring
• sequent calculi
• static analysis
• temporal logics
• term rewriting
• theorem proving
• verification

• Carnegie Mellon University, USA

  Edmund M. Clarke

• School of Computer Science, University of Manchester, Manchester, UK

  Andrei Voronkov

Policies and ethics