Logic for Programming, Artificial Intelligence, and Reasoning

Name: Logic for Programming, Artificial Intelligence, and Reasoning | 18th International Conference, LPAR-18, Merida, Venezuela, March 11-15, 2012, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

18th International Conference, LPAR-18, Merida, Venezuela, March 11-15, 2012, Proceedings

Nikolaj Bjørner Andrei Voronkov(Herausgeber*in)

Springer (Verlag)

Erschienen am 6. März 2012

XI, 446 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-28717-6 (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
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

Systemvoraussetzungen

Als PDF speichern Als Link merken