Logic for Programming, Artificial Intelligence, and Reasoning

Inhaltsverzeichnis

• 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 JavaVerification 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.