Logic for Programming, Artificial Intelligence, and Reasoning
16th International Conference, LPAR-16, Dakar, Senegal, April 25--May 1, 2010, Revised Selected Papers
Published on 7. December 2010
X, 517 pages
978-3-642-17511-4 (ISBN)
Description
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.
More details
Series
Language
English
Place of publication
Berlin
Germany
Publishing group
Springer Berlin
Target group
Professional and scholarly
Illustrations
X, 517 p. 71 illus., 4 illus. in color.
File size
7,86 MB
ISBN-13
978-3-642-17511-4 (9783642175114)
DOI
10.1007/978-3-642-17511-4
Schweitzer Classification
Other editions
Additional editions
Edmund M. Clarke | Andrei Voronkov
Logic for Programming, Artificial Intelligence, and Reasoning
16th International Conference, LPAR-16, Dakar, Senegal, April 25--May 1, 2010, Revised Selected Papers
Book
01/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organisation
- Table of Contents
- The TPTP World - Infrastructure for Automated Reasoning
- Introduction
- The TPTP World Core Infrastructure
- TPTP World Services
- TPTP World Applications
- Current Developments in the TPTP World
- Conclusion
- References
- Speed-Up Techniques for Negation in Grounding
- Introduction
- Background
- Formula Rewriting
- T/F Relational Algebra
- Comparing the Methods: An Example
- Experimental Evaluation
- Conclusions and Future Work
- References
- Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation
- Introduction
- Preliminaries
- Semantics of -Calculus
- CTL Syntax and Semantics
- Model Checking
- Abstract Interpretation
- Abstract Interpretation of -Calculus Semantics
- An Abstract Constraint-Based Domain
- Abstract Domains Based on a State-Space Partitions
- Constraint Representation of Transition Systems
- Constraint Representation of the Semantic Functions
- Implementation
- Computation of and Functions Using Constraint Solvers
- Optimisation of Constraint-Based Evaluation
- Experiments Using an SMT Constraint Solver
- Property-Specific Refinements
- Related Work
- Conclusion
- References
- On the Equality of Probabilistic Terms
- Introduction
- A Motivating Example
- Preliminaries
- Syntax and Semantics
- Syntax
- Semantics
- Satisfaction Problem
- Exclusive or, Concatenation, and Projection
- Exclusive or
- Exclusive or, Concatenation, and Projection
- An Equational Logic for Systems of Equations
- Proof System
- Soundness
- Products
- Example Revisited
- Towards Completeness
- Proof Automation
- Conclusion
- References
- Program Logics for Homogeneous Meta-programming
- Introduction
- The Language
- A Logic for Total Correctness
- Reasoning Examples
- Completeness
- Conclusion
- References
- Verifying Pointer and String Analyses with Region Type Systems
- Introduction
- Featherweight Java with Updates
- Preliminaries
- Syntax
- Semantics
- Class Tables
- Region Type System
- Refined Types and Subtyping
- Annotated Class Tables
- Region Type System
- Interpretation
- Parametrized Region Type System
- Abstraction Principles
- The Parametrized Type System
- Algorithmic Type Checking
- String Analysis
- FJEU with Strings
- Pointer Analysis for String Objects
- String Analysis with Operation Contexts
- Discussion
- References
- ABC: Algebraic Bound Computation for Loops
- Introduction
- Motivating Examples
- ABC: System Description
- ABC-Loops
- The Loop Converter
- The Bound Computer
- Symbolic Solver
- Beyond ABC-Loops
- Experiments
- Conclusions
- References
- Hardness of Preorder Checking for Basic Formalisms
- Introduction
- Preliminaries
- Exptime-Hardness of Problems 1 and 2
- Exptime-Hardness of Problem 1
- Exptime-Hardness of Problem 2
- Additional Hardness Results
- Conclusions
- References
- A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
- Introduction
- Propositional Logic in Deep Inference: The SKS System
- Atomic Flows
- Normalisation Step 1: Simple Form
- Threshold Formulae
- Normalisation Step 2: Cut Elimination
- Final Comments
- References
- Pairwise Cardinality Networks
- Introduction
- Sorting Networks - From Batcher to Parberry
- Sorting Networks - From Parberry Back to Batcher
- The Pairwise Cardinality Network
- A Preliminary Evaluation
- Summary and Conclusion
- References
- Logic and Computation in a Lambda Calculus with Intersection and Union Types
- Introduction
- Intersection and Union Types
- $\UNINTU$ : Curry-Style Type Assignment with Intersections and Unions
- $\UNINT$: Church-Style Typing with Intersections and Unions
- The Proof-Term Calculus $\PROOFIU$
- Typed Terms with Intersections and Unions
- Example of Typing for $\UNINT$
- The Isomorphism between $\UNINTU$ and $\UNINT$
- Type Reconstruction and Type Checking Algorithms
- Reduction in $\UNINT$
- Synchronization
- The Reduction Relation $\churchred$
- Example of Reduction for $\UNINT$ (Continued)
- Properties of $\churchred$
- Deciding Type-Derivation Equality
- Type Theories
- Future Work
- References
- Graded Alternating-Time Temporal Logic
- Introduction
- A Motivating Example
- Preliminaries
- Graded ATL: Definitions
- Fixpoint Characterization
- Comparing the Semantics
- Model Checking
- Model Checking Concurrent Games
- References
- Non-oblivious Strategy Improvement
- Introduction
- Preliminaries
- Snares
- Strategy Improvement
- Strategy Trees
- Profitable Back Edges
- Using Snares to Guide Strategy Improvement
- Comparison with Oblivious Strategy Improvement
- Optimal Switching Policies
- Friedmann's Exponential Time Examples
- Conclusions and Further Work
- References
- A Simple Class of Kripke-Style Models in Which Logic and Computation Have Equal Standing
- Introduction
- The Models, Computation, Logic
- Frames
- $\lambda$-Terms
- The Logic
- Expressivity
- Completeness for $\lambda$-Reduction
- The Axioms, Soundness and Completeness
- Theorems and Admissible Rules
- Soundness
- Completeness
- Conclusion
- Negation and the Liar
- Related Work
- Summary, and Further Work
- References
- Label-Free Proof Systems for IntuitionisticModal Logic $\is$
- Introduction
- The Intuitionistic Modal Logic $\is$
- Label-Free Natural Deduction for $\is$
- The MC-Sequent Structure
- A Natural Deduction System for $\is$
- Natural Deduction Systems for $\sff$ and $\imf$
- A Label-Free Sequent Calculus for $\is$
- Depth-Preserving Admissibility of Weakening and Contraction
- Cut-Elimination in $\gis$
- A New Decision Procedure for $\is$
- Conclusion and Perspectives
- References
- An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory
- Introduction
- Intuitionistic Epistemic Logic for Asynchronous Communication
- Syntax
- Semantics
- Soundness
- Strong Completeness
- Axiom Type for Sequential Consistency
- Soundness
- Strong Completeness
- Waitfree Computation
- Decidability of Solvability of Waitfree Task Specification
- Related Work
- Discussions
- References
- Disunification for Ultimately Periodic Interpretations
- Introduction
- Preliminaries
- Disunification
- The Disunification Algorithm PDU
- Correctness and Termination
- Predicate Completion
- Decidability of the Satisfiability of Equational Formulae
- Implementation
- Conclusion
- References
- Synthesis of Trigger Properties
- Introduction
- Trigger Logic
- Automata onWords and Trees
- Expressiveness
- Synthesis
- Upper Bound
- Lower Bound
- Practice Issues
- References
- Semiring-Induced Propositional Logic: Definition and Basic Algorithms
- Introduction
- Semirings
- Semiring-Induced Propositional Logic
- Syntax
- Semantics
- Applications
- Decision Problems (Abool)
- Summation Problems (Acount)
- Optimization Problems (Amin+, Amax)
- Multi-criteria Optimization Problems (An, Af)
- A DPLL Algorithm for Semiring-Induced Propositional Logic
- Transition Systems
- States in SDPLL Transition Systems
- The Basic SDPLL Procedure
- Extending SAT Techniques
- Backjumping, Learning and Restarts
- Conflict-Driven Backjumping and Learning
- Semirings with Idempotent
- Conclusions and Future Work
- References
- Dafny: An Automatic Program Verifier for Functional Correctness
- Introduction
- Dafny Language Features
- Types
- Pre- and Postconditions
- Ghost State
- Modifications
- Functions
- Specifying Data-Structure Invariants
- Type Parameters
- Sets
- Sequences
- Algebraic Datatypes
- Termination Metrics
- Case Study: Schorr-Waite Algorithm
- Related Work
- Conclusions
- References
- Relentful Strategic Reasoning in Alternating-Time Temporal Logic
- Introduction
- Preliminaries
- Memoryful Alternating-Time Temporal Logic
- Decision Procedures
- Agent-Action Tree Automata with Satellites
- From Path Formulas to Satellites
- Satisfiability
- Model Checking
- References
- Counting and Enumeration Problems with Bounded Treewidth
- Introduction
- Preliminaries
- Counting Problems
- Enumeration Problems
- 3-Colorability
- Conclusion
- References
- The Nullness Analyser of {\sc{julia}}
- Introduction
- An Introductory Example
- Nullness Analysis in {\sc{julia}}
- Nullness Analysis of Local Variables
- Globally non-null Fields
- Locally non-null Fields
- Full Arrays
- Collection Classes
- Construction of the Annotation File
- Conclusion
- References
- Qex: Symbolic SQL Query Explorer
- Introduction
- Preliminaries
- Equational Axioms over Lists
- Equational Axioms and E-Matching in SMT Solvers
- Axioms over Lists
- From SQL to Formulas
- Tables and Table Constraints
- Nullable Values
- Formulas for Queries
- Implementation
- Incremental Table Generation
- Symmetry Breaking Formulas
- Experiments
- Related Work
- Conclusion and Future Work
- References
- Automated Proof Compression by Invention of New Definitions
- Introduction, Motivation, and Related Work
- Problem Statement
- Problem of Proof Compression by New Definitions
- Motivating Example
- Implementation
- The Most Compressing Definition and the Least General Generalization
- Finding the Most Compressing Definition Using Substitution Trees
- Testing
- Testing on the TPTP Library
- Testing on Algebraic Problems
- Examples and Discussion
- A Good and a Bad Example
- Understanding Machine Generated Proofs
- Future Work and Conclusions
- References
- Atomic Cut Introduction by Resolution: Proof Structuring and Compression
- Introduction
- The Sequent Calculus
- TheCIRes Method
- Step 1: Introduction of Atomic Cuts on Top
- Step 2: Extraction of the Struct
- Step 3: Construction of the Swapped Clause Set
- Step 4: Refutation of the Swapped Clause Set by Resolution
- Step 5: Construction of O-Projections
- Step 6: Composing the O-Projections on Top of the Refutation
- Exponential Proof Compression
- Conclusions
- References
- Satisfiability of Non-linear (Ir)rational Arithmetic
- Introduction
- Encoding Non-linear Non-integral Arithmetic
- Rational Arithmetic
- Extending Rational Arithmetic by Roots of Numbers
- Experimental Evaluation
- Comparison with SMT Solvers
- Evaluation within a Termination Prover
- Related Work and Concluding Remarks
- References
- Coping with Selfish On-Going Behaviors
- Introduction
- Preliminaries
- Weighted Finite Automaton
- Input Cheating and Resilience of Automata
- The Cheating-Allowed Automaton
- Resilience Testing
- Hardness Proof for WFA
- A Polynomial Algorithm for DWFA
- Achieving Resilience with Minimum Resources
- Hardness Proof for WFA
- A Polynomial Algorithm for DWFA
- References
- Author Index
