Logic for Programming, Artificial Intelligence, and Reasoning: 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013, Proceedings - Softcover

Softcover

ISBN 10: 3642452221 ISBN 13: 9783642452222

Publisher: Springer, 2013

Synopsis

An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics.- May-Happen-in-Parallel Analysis for Priority-Based Scheduling.- The Complexity of Clausal Fragments of LTL.- A Semantic Basis for Proof Queries and Transformations.- Expressive Path Queries on Graphs with Data.- Proving Infinite Satisfiability.- SAT-Based Preprocessing for MaxSAT.- Dynamic and Static Symmetry Breaking in Answer Set Programming.- HOL Based First-Order Modal Logic Provers.- Resourceful Reachability as HORN-LA.- A Seligman-Style Tableau System.- Comparison of LTL to Deterministic Rabin Automata Translators.- Tree Interpolation in Vampire.- Polarizing Double-Negation Translations.- Revisiting the Equivalence of Shininess and Politeness.- Towards Rational Closure for Fuzzy Logic: The Case of Propositional Gödel Logic.- Multi-objective Discounted Reward Verification in Graphs and MDPs.- Description Logics, Rules and Multi-context Systems.- Complexity Analysis in Presence of Control Operators and Higher-Order Functions.- Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo.- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving.- Verifying Temporal Properties in Real Models.- A Graphical Language for Proof Strategies.- A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus.- Relaxing Synchronization Constraints in Behavioral Programs.- Characterizing Subset Spaces as Bi-topological Structures.- Proof-Pattern Recognition and Lemma Discovery in ACL2.- Semantic A-translations and Super-Consistency Entail Classical Cut Elimination.- Blocked Clause Decomposition.- Maximal Falsifiability: Definitions, Algorithms, and Applications.- Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning.- On QBF Proofs and Preprocessing.- Partial Backtracking in CDCL Solvers.- Lemma Mining over HOL Light.- On Module-Based Abstraction and Repair of Behavioral Programs.- Prediction and Explanation over DL-Lite Data Streams.- Forgetting Concept and Role Symbols in ALCH-Ontologies.- Simulating Parity Reasoning.- Herbrand Theorems for Substructural Logics.- On Promptness in Parity Games.- Defining Privacy Is Supposed to Be Easy.- Reachability Modules for the Description Logic SRIQ.- An Event Structure Model for Probabilistic Concurrent Kleene Algebra.- Three SCC-Based Emptiness Checks for Generalized Büchi Automata.- PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification.- Incremental Tabling for Query-Driven Propagation of Logic Program Updates.- Tracking Data-Flow with Open Closure Types.- Putting Newton into Practice: A Solver for Polynomial Equations over Semirings.- System Description: E 1.8.- Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light.- On Minimality and Integrity Constraints in Probabilistic Abduction.- POLAR: A Framework for Proof Refactoring.

Edition details

• Publisher: Springer
• Publication date: 2013
• ISBN 10: 3642452221
• ISBN 13: 9783642452222
• Binding: Paperback
• Language: English
• Number of pages: 810
• Editor: McMillan Ken, Middeldorp Aart, Voronkov Andrei