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

Front Matter....Pages -
An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics....Pages 1-17
May-Happen-in-Parallel Analysis for Priority-Based Scheduling....Pages 18-34
The Complexity of Clausal Fragments of LTL....Pages 35-52
A Semantic Basis for Proof Queries and Transformations....Pages 53-70
Expressive Path Queries on Graphs with Data....Pages 71-85
Proving Infinite Satisfiability....Pages 86-95
SAT-Based Preprocessing for MaxSAT....Pages 96-111
Dynamic and Static Symmetry Breaking in Answer Set Programming....Pages 112-126
HOL Based First-Order Modal Logic Provers....Pages 127-136
Resourceful Reachability as HORN-LA....Pages 137-146
A Seligman-Style Tableau System....Pages 147-163
Comparison of LTL to Deterministic Rabin Automata Translators....Pages 164-172
Tree Interpolation in Vampire....Pages 173-181
Polarizing Double-Negation Translations....Pages 182-197
Revisiting the Equivalence of Shininess and Politeness....Pages 198-212
Towards Rational Closure for Fuzzy Logic: The Case of Propositional Gödel Logic....Pages 213-227
Multi-objective Discounted Reward Verification in Graphs and MDPs....Pages 228-242
Description Logics, Rules and Multi-context Systems....Pages 243-257
Complexity Analysis in Presence of Control Operators and Higher-Order Functions....Pages 258-273
 Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo....Pages 274-290
Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving....Pages 291-308
Verifying Temporal Properties in Real Models....Pages 309-323
A Graphical Language for Proof Strategies....Pages 324-339
A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus....Pages 340-354
Relaxing Synchronization Constraints in Behavioral Programs....Pages 355-372
Characterizing Subset Spaces as Bi-topological Structures....Pages 373-388
Proof-Pattern Recognition and Lemma Discovery in ACL2....Pages 389-406
Semantic A-translations and Super-Consistency Entail Classical Cut Elimination....Pages 407-422
Blocked Clause Decomposition....Pages 423-438
Maximal Falsifiability....Pages 439-456
Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning....Pages 457-472
On QBF Proofs and Preprocessing....Pages 473-489
Partial Backtracking in CDCL Solvers....Pages 490-502
Lemma Mining over HOL Light ....Pages 503-517
On Module-Based Abstraction and Repair of Behavioral Programs....Pages 518-535
Prediction and Explanation over DL- Lite Data Streams....Pages 536-551
Forgetting Concept and Role Symbols in $\mathcal{ALCH}$ -Ontologies....Pages 552-567
Simulating Parity Reasoning....Pages 568-583
Herbrand Theorems for Substructural Logics....Pages 584-600
On Promptness in Parity Games....Pages 601-618
Defining Privacy Is Supposed to Be Easy....Pages 619-635
Reachability Modules for the Description Logic $\mathcal{SRIQ}$ ....Pages 636-652
An Event Structure Model for Probabilistic Concurrent Kleene Algebra....Pages 653-667
Three SCC-Based Emptiness Checks for Generalized Büchi Automata....Pages 668-682
PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification....Pages 683-693
Incremental Tabling for Query-Driven Propagation of Logic Program Updates....Pages 694-709
Tracking Data-Flow with Open Closure Types....Pages 710-726
Putting Newton into Practice: A Solver for Polynomial Equations over Semirings....Pages 727-734
System Description: E 1.8....Pages 735-743
Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light....Pages 744-758
On Minimality and Integrity Constraints in Probabilistic Abduction....Pages 759-775
 Polar : A Framework for Proof Refactoring....Pages 776-791
Back Matter....Pages -