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

PROGRAM

Saturday, December 14th, 2013

Saturday's program is also available with abstracts.

08:30-09:30 Session 1 (ALCS)
08:30
On the Algebraization of Non-finitary Logics (abstract)
09:00
On Deductive Systems Associated with Equationally Orderable Quasivarieties (abstract)
09:30-10:00Coffee Break
10:00-12:00 Session 2A (ALFA)
10:00
Some Algebraic Means for Characterizing Logics (abstract)
10:30
Software Model Synthesis using Satisfiability Solvers (abstract)
11:00
Strategic Reasoning in Formal Verification (abstract)
11:30
Automata Reasoning via First-order Superposition (abstract)
10:00-12:00 Session 2B (ALCS)
10:00
The Quest for the Basic Fuzzy Logic (abstract)
10:30
Short Communication: Complete MV-Algebra Valued Pavelka Logic (abstract)
11:00
Co-Rotation, Co-Rotation-Annihilation, and Involutive Ordinal Sum Constructions of Residuated Semigroups (abstract)
11:30
Discrete Dualities for n-potent MTL and BL-Algebras (abstract)
12:00-14:00Lunch
14:00-15:30 Session 3A (ALFA)
14:00
Growth in Hecke groups (abstract)
14:30
Newton's Method on Commutative Semirings, Tree Dimension, and Applications (abstract)
15:00
Ehrenfeucht-Fraisse Games on Omega-Terms (abstract)
14:00-15:30 Session 3B (IWIL)
14:00
The TPTP Process Instruction Language (abstract)
14:30
Gödel's God on the Computer (abstract)
14:00-15:30 Session 3C: Logics and Reasoning for Conceptual Modeling (LRCM)
14:00
Answering queries over inconsistent databases (abstract)
15:00
Scenario Testing on UML Class Diagrams using Description Logic (abstract)
14:00-15:30 Session 3D (ALCS)
14:00
Representations for Ramsey Relation Algebras (abstract)
14:30
An Isomorphism Criterion for Colimits of Sequences of Finitely Presented Objects (abstract)
15:00
A Completeness Theorem for Two-Layer Modal Logics (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 4A (IWIL)
16:00
An Interactive Prover for Bi-Intuitionistic Logic (abstract)
16:30
Towards Explicit Rewrite Rules in the Lambda-Pi Calculus Modulo (abstract)
17:00
Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps (abstract)
16:00-17:00 Session 4B (ALCS)
16:00
Algorithmic-Algebraic Canonicity for Mu-Calculi (abstract)
16:30
Cut-free Calculi for Challenge Logics in a Lazy Way (abstract)
16:00-17:00 Session 4C (LRCM)
16:00
Toward Representing Attributes in Temporal Conceptual Data Models (abstract)
16:30
Defeasible ORM2 Constraints to Preserve Coherence (Extended Abstract) (abstract)
Sunday, December 15th, 2013

Sunday's program is also available with abstracts.

08:30-09:30 Session 5: Invited talk by Toby Walsh (LPAR)
08:30
Decomposition in SAT (or why we sometimes need constraint programming) (abstract)
09:30-10:00Coffee Break
10:00-12:00 Session 6 (LPAR)
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 (LPAR)
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 (LPAR)
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 (LPAR)
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 (LPAR)
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 (LPAR)
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 (LPAR)
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 (LPAR)
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 (LPAR)
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 (LPAR)
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 (LPAR)
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 (LPAR)
09:00
Where, What, and How? Lessons from the Evolution of E (abstract)
10:00-10:30Coffee Break
10:30-12:00 Session 18 (LPAR)
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 (LPAR)
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 (LPAR)
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)