Logic for Programming, Artificial Intelligence, and Reasoning

Name: Logic for Programming, Artificial Intelligence, and Reasoning | 16th International Conference, LPAR-16, Dakar, Senegal, April 25--May 1, 2010, Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

16th International Conference, LPAR-16, Dakar, Senegal, April 25--May 1, 2010, Revised Selected Papers

Edmund M. Clarke Andrei Voronkov(Herausgeber*in)

Springer (Verlag)

Erschienen am 7. Dezember 2010

X, 517 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-17511-4 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken