Logic for Programming, Artificial Intelligence, and Reasoning 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005. Proceedings /
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2005.
|
| Σειρά: | Lecture Notes in Computer Science,
3835 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- Independently Checkable Proofs from Decision Procedures: Issues and Progress
- Zap: Automated Theorem Proving for Software Analysis
- Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
- Scaling Up: Computers vs. Common Sense
- A New Constraint Solver for 3D Lattices and Its Application to the Protein Folding Problem
- Disjunctive Constraint Lambda Calculi
- Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search Trees
- The nomore?+?+ Approach to Answer Set Solving
- Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages
- The Four Sons of Penrose
- An Algorithmic Account of Ehrenfeucht Games on Labeled Successor Structures
- Second-Order Principles in Specification Languages for Object-Oriented Programs
- Strong Normalization of the Dual Classical Sequent Calculus
- Termination of Fair Computations in Term Rewriting
- On Confluence of Infinitary Combinatory Reduction Systems
- Matching with Regular Constraints
- Recursive Path Orderings Can Also Be Incremental
- Automating Coherent Logic
- The Theorema Environment for Interactive Proof Development
- A First Order Extension of Stålmarck’s Method
- Regular Derivations in Basic Superposition-Based Calculi
- On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity
- Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
- Monotone AC-Tree Automata
- On the Specification of Sequent Systems
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- Integration of a Software Model Checker into Isabelle
- Experimental Evaluation of Classical Automata Constructions
- Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
- Reasoning About Incompletely Defined Programs
- Model Checking Abstract State Machines with Answer Set Programming
- Characterizing Provability in BI’s Pointer Logic Through Resource Graphs
- A Unified Memory Model for Pointers
- Treewidth in Verification: Local vs. Global
- Pushdown Module Checking
- Functional Correctness Proofs of Encryption Algorithms
- Towards Automated Proof Support for Probabilistic Distributed Systems
- Algebraic Intruder Deductions
- Satisfiability Checking for PC(ID)
- Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
- Another Complete Local Search Method for SAT
- Inference from Controversial Arguments
- Programming Cognitive Agents in Defeasible Logic
- The Relationship Between Reasoning About Privacy and Default Logics
- Comparative Similarity, Tree Automata, and Diophantine Equations
- Analytic Tableaux for KLM Preferential and Cumulative Logics
- Bounding Resource Consumption with Gödel-Dummett Logics
- On Interpolation in Existence Logics
- Incremental Integrity Checking: Limitations and Possibilities
- Concepts of Automata Construction from LTL.
