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

Chair: Aart Middeldorp

08:30

Toby Walsh

Decomposition in SAT (or why we sometimes need constraint programming) (abstract)

09:30-10:00Coffee Break

10:00-12:00 Session 6

Chair: Geoff Sutcliffe

10:00	Stephan Schulz System Description: E 1.8 (abstract)
10:20	Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson and Ewen MacLean Proof-Pattern Recognition and Lemma Discovery in ACL2 (abstract)
10:40	Gudmund Grov, Aleks Kissinger and Yuhui Lin A Graphical Language for Proof Strategies (abstract)
11:00	David Aspinall, Ewen Denney and Christoph Lüth A Semantic Basis for Proof Queries and Transformations (abstract)
11:20	Hira Taqdees and Osman Hasan Formalization of Laplace Transform using the Multivariable Calculus Theory of HOL-Light (abstract)
11:40	Cezary Kaliszyk and Josef Urban Lemma Mining over HOL Light (abstract)

12:00-14:00Lunch

14:00-15:30 Session 7: Temporal Logic

Chair: Cezary Kaliszyk

14:00	Fabio Mogavero, Aniello Murano and Loredana Sorrentino On Promptness in Parity Games (abstract)
14:20	František Blahoudek, Jan Strejcek and Mojmir Kretinsky Comparison of LTL to Deterministic Rabin Automata Translators (abstract)
14:40	Patrick Doherty, Fredrik Heintz and Jonas Kvarnström Robotics, Temporal Logic and Stream Reasoning (abstract)
14:50	Tim French, John Mccabe-Dansted and Mark Reynolds Verifying Temporal Properties in Real Models (abstract)
15:10	Pablo Barceló, Gaelle Fontaine and Anthony Widjaja Lin Expressive Path Queries on Graphs with Data (abstract)

15:30-16:00Coffee Break

16:00-17:30 Session 8

Chair: Toby Walsh

16:00	Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Hyvaerinen and Natasha Sharygina PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification (abstract)
16:20	Alexey Ignatiev, Antonio Morgado, Jordi Planes and Joao Marques-Silva Maximal Falsifiability: Definitions, Algorithms, and Applications (abstract)
16:40	Guy Katz On Module-based Abstraction and Repair of Behavioral Programs (abstract)
17:00	Chuan Jiang and Ting Zhang Partial Backtracking in CDCL Solvers (abstract)
17:20	Francesco Alberti, Silvio Ghilardi and Natasha Sharygina 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

Chair: Zoltan Esik

09:00

Volker Diekert

The Local Divisor Approach to First-Order Languages (abstract)

10:00-10:30Coffee Break

10:30-12:00 Session 10: Interpolation and SMT

Chair: Christoph Benzmueller

10:30	Régis Blanc, Ashutosh Gupta, Laura Kovacs and Bernhard Kragl Tree Interpolation in Vampire (abstract)
10:50	Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin and Ori Lahav Instantiations, Zippers and EPR Interpolation (abstract)
11:00	Filipe Casal and João Rasga Revisiting the Equivalence of Shininess and Politeness (abstract)
11:20	Josh Berdine, Nikolaj Bjorner, Samin Ishtiaq, Jael Kriener and Christoph Wintersteiger Resourceful Reachability as HORN-LRA (abstract)
11:40	Peter Baumgartner and Joshua Bax Proving Infinite Satisfiability (abstract)

12:00-14:00Lunch

14:00-15:30 Session 11

Chair: Michel Parigot

14:00	Ari Saptawijaya and Luís Moniz Pereira Incremental Tabling for Query-Driven Propagation of Logic Program Updates (abstract)
14:20	Calin-Rares Turliuc, Nataly Maimari, Alessandra Russo and Krysia Broda On Minimality and Integrity Constraints in Probabilistic Abduction (abstract)
14:40	Petr Cintula and George Metcalfe Herbrand Theorems for Substructural Logics (abstract)
15:00	Jiefei Ma, Rob Miller, Leora Morgenstern and Theodore Patkos An Epistemic Event Calculus for ASP-based Reasoning About Knowledge of the Past, Present and Future (abstract)
15:10	Sebastian A. Mödersheim, Thomas Gross and Luca Viganò Defining Privacy is Supposed to be Easy (abstract)

15:30-16:00Coffee Break

16:00-18:00 Session 12

Chair: Peter Baumgartner

16:00	David Harel, Amir Kantor and Guy Katz Relaxing Synchronization Constraints in Behavioral Programs (abstract)
16:20	Maximilian Schlund, Michal Terepeta and Michael Luttenberger Putting Newton into Practice: A Solver for Polynomial Equations over Semirings (abstract)
16:40	Shachar Itzhaky, Sumit Gulwani, Neil Immerman and Mooly Sagiv Solving Geometry Problems using a Combination of Symbolic and Numerical Reasoning (abstract)
17:00	Elvira Albert, Samir Genaim and Enrique Martin-Martin May-Happen-in-Parallel Analysis for Priority-based Scheduling (abstract)
17:20	Tahiry Rabehaja, Annabelle McIver and Georg Struth An Event Structure Model for Probabilistic Concurrent Kleene Algebra (abstract)
17:40	Anton Belov, António Morgado and Joao Marques-Silva 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

Chair: Konstantin Korovin

09:00

Frank Wolter

Ontology-based Data Access: A Study through Disjunctive Datalog, CSP, and MMSNP (abstract)

10:00-10:30Coffee Break

10:30-12:00 Session 14

Chair: Margus Veanes

10:30	Krishnendu Chatterjee, Vojtech Forejt and Dominik Wojtczak Multi-Objective Discounted Reward Verification in Graphs and MDPs (abstract)
10:50	Martin Baláž, Jozef Frtús and Martin Homola Conflict Resolution in Structured Argumentation (abstract)
11:00	Giovanni Casini and Umberto Straccia Towards Rational Closure for Fuzzy Logic: The Case of Propositional Gödel Logic (abstract)
11:20	Luís Cruz-Filipe, Rita Henriques and Isabel Nunes Description Logics, Rules and Multi-Context Systems (abstract)
11:40	Christoph Benzmueller and Thomas Raths HOL based First-order Modal Logic Provers (abstract)

12:00-14:00Lunch

14:00-15:30 Session 15

Chair: Frank Wolter

14:00	Riku Nortje, Arina Britz and Thomas Meyer Reachability Modules for the Description Logic SRIQ (abstract)
14:20	Patrick Koopmann and Renate A. Schmidt Forgetting Concept and Role Symbols in ALCH-Ontologies (abstract)
14:40	Szymon Klarman and Thomas Meyer Prediction and Explanation over DL-Lite Data Streams (abstract)
15:00	Szymon Klarman Practical Querying of Temporal Data via OWL 2 QL and SQL:2011 (abstract)
15:10	Luca Aceto, Dario Della Monica, Anna Ingolfsdottir, Angelo Montanari and Guido Sciavicco 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

Chair: Laura Kovacs

16:00	Mikolas Janota, Radu Grigore and Joao Marques-Silva On QBF Proofs and Preprocessing (abstract)
16:20	Tero Laitinen, Tommi Junttila and Ilkka Niemelä Simulating Parity Reasoning (abstract)
16:40	Manuel Lamotte-Schubert and Christoph Weidenbach BDI: A New Decidable First-order Clause Class (abstract)
16:50	Marijn Heule and Armin Biere Blocked Clause Decomposition (abstract)
17:10	Uwe Egly, Florian Lonsing and Magdalena Widl 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

Chair: Andrei Voronkov

09:00

Stephan Schulz

Where, What, and How? Lessons from the Evolution of E (abstract)

10:00-10:30Coffee Break

10:30-12:00 Session 18

Chair: Krysia Broda

10:30	Mélanie Boudard and Olivier Hermant Polarizing Double Negation Translations (abstract)
10:50	Tom Gundersen, Willem Heijltjes and Michel Parigot A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus (abstract)
11:10	Ugo Dal Lago and Giulio Pellitta Complexity Analysis in Presence of Control Operators and Higher-order Functions (abstract)
11:30	Olivier Hermant and Allali Lisa Semantic A-Translations and Super-Consistency entail Classical Cut Elimination (abstract)
11:50	Margus Veanes, Nikolaj Bjorner, Lev Nachmanson and Sergey Bereg Effectively Monadic Predicates (abstract)

12:00-14:00Lunch

14:00-15:30 Session 19

Chair: Ewen Denney

14:00	Gabriel Aranda, Susana Nieva, Fernando Saenz-Perez and Jaime Sánchez-Hernández Incorporating Hypothetical Views and Extended Recursion into SQL Database Systems (abstract)
14:10	David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand and Olivier Hermant Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo (abstract)
14:30	Iain Whiteside, Dominik Dietrich and David Aspinall Polar: A Framework for Proof Refactoring (abstract)
14:50	Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov and Michael Zakharyaschev The Complexity of Clausal Fragments of LTL (abstract)
15:10	Patrick Blackburn, Thomas Bolander, Torben Braüner and Klaus Frovin Joergensen A Seligman-style Tableau System (abstract)

15:30-16:00Coffee Break

16:00-17:30 Session 20

Chair: Volker Diekert

16:00	Belaïd Benhamou Dynamic and static symmetry breaking in answer set programming (abstract)
16:20	Gabriel Scherer and Jan Hoffmann Tracking Data-Flow with Open Closure Types (abstract)
16:40	Bernhard Heinemann Characterizing Subset Spaces as Bi-Topological Structures (abstract)
17:00	Abhijeet Mohapatra and Michael Genesereth An Incremental Algorithm to Optimally Maintain Aggregate Views (abstract)
17:10	Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon and Denis Poitrenaud Three SCC-based Emptiness Checks for Generalized Büchi Automata (abstract)