Logic for Programming, Artificial Intelligence, and Reasoning
18th International Conference, LPAR-18, Merida, Venezuela, March 11-15, 2012, Proceedings
Published on 6. March 2012
XI, 446 pages
978-3-642-28717-6 (ISBN)
Description
This book constitutes the proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18, held in Merida, Venezuela, in March 2012. The 25 regular papers and 6 tool descriptions and experimental papers presented were carefully reviewed and selected from 74 submissions.
The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world.
More details
Other editions
Additional editions
Nikolaj Bjørner | Andrei Voronkov
Logic for Programming, Artificial Intelligence, and Reasoning
18th International Conference, LPAR-18, Merida, Venezuela, March 11-15, 2012, Proceedings
Book
02/2012
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Automatic Inference of Resource Consumption Bounds
- Introduction
- Generation of Cost Relations
- Inference of Closed-Form Bounds
- Modularity and Incrementality
- Memory Consumption Analysis for Garbage-Collected Languages
- Concurrency in Cost Analysis
- Certified Resource Bounds
- Conclusions and Future Work
- References
- Matrix Interpretations for Polynomial Derivational Complexity of Rewrite Systems
- References
- Parameterized Complexity and Fixed-Parameter Tractability of Description Logic Reasoning
- References
- Enfragmo: A System for Modelling and Solving Search Problems with Logic
- Introduction
- Specification Language
- Implementation
- Experimental Evaluation
- Conclusion
- References
- The Permutative ?-Calculus
- Introduction
- The Permutative ?-Calculus
- Towards Confluence of ß/P
- The Auxiliary sub-Calculus
- The Z-property Modulo by Means of M-developments
- Adding the Unboxing Rule
- Preservation of ß-Strong Normalisation
- Conclusions and Future Work
- References
- Automated and Human Proofs in General Mathematics: An Initial Comparison
- Introduction: Automated Theorem Proving in Mathematics
- Finding Proofs in the MML with AI/ATP Support
- Mining the Minimal Dependencies from All Human-Written MML Proofs
- Learning Premise Selection from Proof Dependencies
- Using ATPs to Prove the Conjectures from the Selected Premises
- Proof Metrics
- Evaluation
- Comparing Weights
- Conclusion
- References
- Lazy Abstraction with Interpolants for Arrays
- Introduction
- Background Notions on MCMT
- Unwinding Array-Based Systems
- Lazy Abstraction with Interpolants in MCMT
- Completeness and Termination
- Implementation and Experiments
- Conclusion
- References
- Backward Trace Slicing for Conditional Rewrite Theories
- Introduction
- Preliminaries
- Conditional Rewriting Modulo Equational Theories
- Backward Conditional Slicing
- Term Slices and Term Slice Concretizations
- Backward Slicing for Execution Traces
- The Function slice-step
- Implementation and Experimental Evaluation
- References
- Forgetting for Defeasible Logic
- Introduction
- Defeasible Logic
- Forgetting in Defeasible Logic: A Naive Approach
- Forgetting in Defeasible Logic: An Improved Approach
- Semantic Properties
- Complexity
- Modularity
- Conclusion
- References
- Querying Proofs
- Introduction
- Hiproofs
- Local Structured Queries
- Examples
- Semantics
- Examples and Their Results
- Query Equivalence and Decidability
- Implementing Queries
- Related Work and Conclusions
- References
- Solving Language Equations and Disequations with Applications to Disunification in Description Logics and Monadic Set Constraints
- Introduction
- Language (Dis)equations With One-Sided Concatenation
- The Problem Definition
- Translation into Looping Tree Automata
- Looping Tree Automata with Colors
- Decidability of the Emptiness Problem
- The Exact Complexity of the Emptiness Problem
- Applying the Results
- Disunification in FL0
- Monadic Set Constraints
- Conclusion
- References
- Dual-Priced Modal Transition Systems with Time Durations
- Introduction and Motivating Example
- Modal Transition Systems with Durations
- Dual-Price Scheme
- Complexity Results
- Weighted Mean Payoff Games
- Translating Dual-Priced MTSD into Weighted MPG
- Optimizations
- The Algorithm and Its Complexity
- Conclusion and Future Work
- References
- Finding Finite Herbrand Models
- Introduction
- Propagation Rules
- Propagation Nets
- Behavior of Propagation Nets
- Deciding Termination
- Hardness
- Summary and Conclusions
- References
- Smart Testing of Functional Programs in Isabelle
- Introduction
- Related Work
- Motivation
- Overview of the Tool
- Design Decisions
- Architecture
- Preprocessing
- Mode Analysis
- Generator Compilation
- Evaluation
- Conclusion
- References
- Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic
- Introduction
- Weighted Timed Automata and Metric Temporal Logic
- Weighted Timed Automata
- Monitoring Weighted Timed Automata
- Weighted Metric Temporal Logic WMTL
- From Formulas to Monitors
- Closures and Extended Formulas
- Constructing Non-deterministic Monitors
- Constructing Deterministic Monitors
- The Tool Chain
- Case Studies
- Automatically Generated Formulas
- Robot Control
- Related and Future Work
- References
- Duality between Merging Operators and Social Contraction Operators
- Introduction
- Preliminaries
- Merging Operators
- Social Contraction Operators
- Duality
- Concluding Remarks
- References
- Automatic Generation of Invariants for Circular Derivations in SUP(LA)
- Introduction
- Preliminaries
- Constraint Induction
- Finite Saturation of Extended Timed Automata
- Implementation and Results
- Conclusion
- References
- Moral Reasoning under Uncertainty
- Introduction
- The Trolley Problem and the Principle of Double Effect
- Evolution Prospection under Uncertainty with P-log
- Evolution Prospection
- P-log
- Moral Reasoning under Uncertainty
- Revised Bystander Case
- Revised Footbridge Case
- Moral Reasoning Concerning Uncertain Actions
- Discussion
- Conclusions
- References
- Towards Algorithmic Cut-Introduction
- Introduction
- Proofs and Herbrand-Sequents
- Cut-Elimination and Cut-Introduction
- A Calculus of Decompositions
- Computing the Propositional Structure
- Improving the Canonical Solution
- Conclusion
- References
- Conflict Anticipation in the Search for Graph Automorphisms
- Introduction
- Preliminaries
- Baseline Algorithms
- Conflict Anticipation via Simultaneous Refinement
- The Validity of Matching OPP Pruning
- Experimental Evaluation
- Conclusions
- References
- Confluence of Non-Left-Linear TRSs via Relative Termination
- Introduction
- Preliminaries
- Confluence Criterion
- Joinability of S-Critical Pairs
- Experiments
- Implementation
- Experimental Results
- Related Work
- Conclusion
- References
- Regular Expressions for DataWords
- Introduction
- Register Automata over Data Words
- Regular Expressions with Memory
- Equivalence with Register Automata
- Properties of Regular Expressions with Memory
- Regular Expressions with Equality
- Properties of Regular Expressions with Equality
- Conclusions and Future Work
- References
- Automatic Verification of TLA+ Proof Obligations with SMT Solvers
- Introduction
- TLA+ and the SMT Languages
- The Non-temporal Fragment of TLA+
- Input Languages of SMT Solvers
- Type Inference for TLA+
- From TLA+ to SMT
- Experimental Results
- Conclusions
- References
- An Asymptotically Correct Finite Path Semantics for LTL
- Introduction
- Syntax and Semantics of LTL
- Previous Definitions of LTL on Finite Paths
- LTL3
- FLTL
- Problems with RV-LTL
- Asymptotic Finite Linear Temporal Logic (RV-LTL)
- The Temporal Logic Classes RV-TLG and RV-TLF
- The Temporal Logic RV-TLF G
- Asymptotic Correctness
- The Temporal Logic RV-TLG F
- The Temporal Logic RV-TLStreett
- Conclusion
- References
- On the Domain and Dimension Hierarchy of Matrix Interpretations
- Introduction
- Preliminaries
- Linear Algebra
- Term Rewriting
- Monotone Algebras and Matrix Interpretations
- TheDomainHierarchy
- Matrix Interpretations over Q
- Matrix Interpretations over R
- The Dimension Hierarchy
- Conclusion
- References
- iSat: Structure Visualization for SAT Problems
- Introduction
- A Brief Overview on SAT Solving
- A Sample Session
- Services Provided by iSat
- Extending iSat
- Conclusions
- References
- Linear Constraints over Infinite Trees
- Introduction
- Infinite Trees
- Constraints
- Algorithmic Problems
- Solving a System of Constraints
- Tree Schema Substitution and Ts(C)
- Computation of Ts(C)
- Linear Constraint System (LCS)
- Elimination of Tree Variables
- Applications to Resource Analysis
- Conclusions
- References
- E-Matching with Free Variables
- Introduction
- Introductory Example
- Background
- Syntax and Semantics of Considered Logics
- Sequent Calculi with Constraints
- The Basic Calculus for Function-Free First-Order Logic
- Positive Unit Hyper-Resolution
- E-Matching through Relational Encoding
- Relational Encoding of Functions
- Ground Reasoning and Congruence Closure
- Relational E-Matching and Free Variables to Handle Quantifiers
- Extension to Linear Integer Arithmetic
- Hyper-Resolution and E-Matching for FOL(LIA)
- Experiments and Related Work
- References
- Random: R-Based Analyzer for Numerical Domains
- Introduction
- Template Parallelotopes
- Multiple Template Parallelotopes
- Parallelotope Abstract Domain
- The Tool Interface
- Implementation Details
- Conclusion and Future Work
- References
- Solving Graded/Probabilistic Modal Logic via Linear Inequalities (System Description)
- Syntax, Semantics and Tableau Calculus
- Implementation Details
- Experimental Evaluation
- Conclusion
- References
- Labelled Superposition for PLTL
- Introduction
- Preliminaries
- Labelled Clauses
- The Labelled Superposition Calculus LPSup
- Decision Procedure
- Redundancy, Completeness and Model Building
- Final Discussion and Experiments
- Conclusion
- References
- The TPTP Typed First-Order Form with Arithmetic
- Motivation and History
- The TPTP Typed First-Order Form Language
- Decisions About Types and Terms
- Syntax
- Type Checking and Semantics
- TPTP Arithmetic
- Syntax
- Semantics
- Solvability and Decidability
- TFF Problems, ATP Systems, TPTP Software
- Conclusion
- References
- Ordinals and Knuth-Bendix Orders
- Introduction
- Preliminaries
- KBO
- Transfinite KBO
- Generalized KBO
- Implementation and Evaluation
- Conclusion
- References
- r-TuBound: Loop Bounds for WCET Analysis (Tool Paper)
- Introduction
- r-TuBound: Tool Description and Usage
- Workflow
- Loop Restrictions
- Program Flow Refinement
- Pattern-Based Recurrence Solving
- r-TuBound: Experimental Results
- Conclusion
- References
- Author Index
