19TH INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

LPAR PROGRAM

Sunday, December 15th, 2013

Sunday's program is also available with abstracts.

08:30-09:30 Session 5: Invited talk by Toby Walsh
08:30
Decomposition in SAT (or why we sometimes need constraint programming) (abstract)
09:30-10:00Coffee Break
10:00-12:00 Session 6
10:00
System Description: E 1.8 (abstract)
10:20
Proof-Pattern Recognition and Lemma Discovery in ACL2 (abstract)
10:40
A Graphical Language for Proof Strategies (abstract)
11:00
A Semantic Basis for Proof Queries and Transformations (abstract)
11:20
Formalization of Laplace Transform using the Multivariable Calculus Theory of HOL-Light (abstract)
11:40
Lemma Mining over HOL Light (abstract)
12:00-14:00Lunch
14:00-15:30 Session 7: Temporal Logic
14:00
On Promptness in Parity Games (abstract)
14:20
Comparison of LTL to Deterministic Rabin Automata Translators (abstract)
14:40
Robotics, Temporal Logic and Stream Reasoning (abstract)
14:50
Verifying Temporal Properties in Real Models (abstract)
15:10
Expressive Path Queries on Graphs with Data (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 8
Chair: Toby Walsh
16:00
PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification (abstract)
16:20
Maximal Falsifiability: Definitions, Algorithms, and Applications (abstract)
16:40
On Module-based Abstraction and Repair of Behavioral Programs (abstract)
17:00
Partial Backtracking in CDCL Solvers (abstract)
17:20
Acceleration-based Safety Decision Procedure for Programs with Arrays (abstract)
Monday, December 16th, 2013

Monday's program is also available with abstracts.

09:00-10:00 Session 9: Invited talk by Volker Diekert
09:00
The Local Divisor Approach to First-Order Languages (abstract)
10:00-10:30Coffee Break
10:30-12:00 Session 10: Interpolation and SMT
10:30
Tree Interpolation in Vampire (abstract)
10:50
Instantiations, Zippers and EPR Interpolation (abstract)
11:00
Revisiting the Equivalence of Shininess and Politeness (abstract)
11:20
Resourceful Reachability as HORN-LRA (abstract)
11:40
Proving Infinite Satisfiability (abstract)
12:00-14:00Lunch
14:00-15:30 Session 11
14:00
Incremental Tabling for Query-Driven Propagation of Logic Program Updates (abstract)
14:20
On Minimality and Integrity Constraints in Probabilistic Abduction (abstract)
14:40
Herbrand Theorems for Substructural Logics (abstract)
15:00
An Epistemic Event Calculus for ASP-based Reasoning About Knowledge of the Past, Present and Future (abstract)
15:10
Defining Privacy is Supposed to be Easy (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 12
16:00
Relaxing Synchronization Constraints in Behavioral Programs (abstract)
16:20
Putting Newton into Practice: A Solver for Polynomial Equations over Semirings (abstract)
16:40
Solving Geometry Problems using a Combination of Symbolic and Numerical Reasoning (abstract)
17:00
May-Happen-in-Parallel Analysis for Priority-based Scheduling (abstract)
17:20
An Event Structure Model for Probabilistic Concurrent Kleene Algebra (abstract)
17:40
SAT Preprocessing for MaxSAT (abstract)
Wednesday, December 18th, 2013

Wednesday's program is also available with abstracts.

09:00-10:00 Session 13: Invited talk by Frank Wolter
09:00
Ontology-based Data Access: A Study through Disjunctive Datalog, CSP, and MMSNP (abstract)
10:00-10:30Coffee Break
10:30-12:00 Session 14
10:30
Multi-Objective Discounted Reward Verification in Graphs and MDPs (abstract)
10:50
Conflict Resolution in Structured Argumentation (abstract)
11:00
Towards Rational Closure for Fuzzy Logic: The Case of Propositional Gödel Logic (abstract)
11:20
Description Logics, Rules and Multi-Context Systems (abstract)
11:40
HOL based First-order Modal Logic Provers (abstract)
12:00-14:00Lunch
14:00-15:30 Session 15
14:00
Reachability Modules for the Description Logic SRIQ (abstract)
14:20
Forgetting Concept and Role Symbols in ALCH-Ontologies (abstract)
14:40
Prediction and Explanation over DL-Lite Data Streams (abstract)
15:00
Practical Querying of Temporal Data via OWL 2 QL and SQL:2011 (abstract)
15:10
An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 16
16:00
On QBF Proofs and Preprocessing (abstract)
16:20
Simulating Parity Reasoning (abstract)
16:40
BDI: A New Decidable First-order Clause Class (abstract)
16:50
Blocked Clause Decomposition (abstract)
17:10
Long-distance Resolution: Proof Generation and Strategy Extraction in Search-based QBF Solving (abstract)
Thursday, December 19th, 2013

Thursday's program is also available with abstracts.

09:00-10:00 Session 17: Invited talk by Stephan Schulz
09:00
Where, What, and How? Lessons from the Evolution of E (abstract)
10:00-10:30Coffee Break
10:30-12:00 Session 18
10:30
Polarizing Double Negation Translations (abstract)
10:50
A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus (abstract)
11:10
Complexity Analysis in Presence of Control Operators and Higher-order Functions (abstract)
11:30
Semantic A-Translations and Super-Consistency entail Classical Cut Elimination (abstract)
11:50
Effectively Monadic Predicates (abstract)
12:00-14:00Lunch
14:00-15:30 Session 19
14:00
Incorporating Hypothetical Views and Extended Recursion into SQL Database Systems (abstract)
14:10
Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo (abstract)
14:30
Polar: A Framework for Proof Refactoring (abstract)
14:50
The Complexity of Clausal Fragments of LTL (abstract)
15:10
A Seligman-style Tableau System (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 20
16:00
Dynamic and static symmetry breaking in answer set programming (abstract)
16:20
Tracking Data-Flow with Open Closure Types (abstract)
16:40
Characterizing Subset Spaces as Bi-Topological Structures (abstract)
17:00
An Incremental Algorithm to Optimally Maintain Aggregate Views (abstract)
17:10
Three SCC-based Emptiness Checks for Generalized Büchi Automata (abstract)