PROGRAM

Saturday, December 14th, 2013

Saturday's program is also available with abstracts.

08:30	James Raftery On the Algebraization of Non-finitary Logics (abstract)
09:00	Ramon Jansana On Deductive Systems Associated with Equationally Orderable Quasivarieties (abstract)

09:30-10:00Coffee Break

10:00-12:00 Session 2A (ALFA)

Chair: Manfred Kufleitner

10:00	Zoltan Esik Some Algebraic Means for Characterizing Logics (abstract)
10:30	Marijn Heule Software Model Synthesis using Satisfiability Solvers (abstract)
11:00	Aniello Murano Strategic Reasoning in Formal Verification (abstract)
11:30	Christoph Weidenbach Automata Reasoning via First-order Superposition (abstract)

10:00-12:00 Session 2B (ALCS)

Chair: Petr Cintula

10:00	Petr Cintula, Rostislav Horcik and Carles Noguera The Quest for the Basic Fuzzy Logic (abstract)
10:30	Esko Turunen Short Communication: Complete MV-Algebra Valued Pavelka Logic (abstract)
11:00	Sándor Jenei Co-Rotation, Co-Rotation-Annihilation, and Involutive Ordinal Sum Constructions of Residuated Semigroups (abstract)
11:30	Ivo Duntsch, Ewa Orlowska and Clint Van Alten Discrete Dualities for n-potent MTL and BL-Algebras (abstract)

12:00-14:00Lunch

14:00-15:30 Session 3A (ALFA)

Chair: Volker Diekert

14:00	Gerhard Rosenberger Growth in Hecke groups (abstract)
14:30	Maximilian Schlund Newton's Method on Commutative Semirings, Tree Dimension, and Applications (abstract)
15:00	Manfred Kufleitner Ehrenfeucht-Fraisse Games on Omega-Terms (abstract)

14:00-15:30 Session 3B (IWIL)

Chair: Stephan Schulz

14:00	Geoff Sutcliffe The TPTP Process Instruction Language (abstract)
14:30	Christoph Benzmueller and Bruno Woltzenlogel Paleo Gödel's God on the Computer (abstract)

14:00-15:30 Session 3C: Logics and Reasoning for Conceptual Modeling (LRCM)

Chair: C. Maria Keet

14:00	Gaelle Fontaine Answering queries over inconsistent databases (abstract)
15:00	Hendrina F. Harmse, Arina Britz and Aurona Gerber Scenario Testing on UML Class Diagrams using Description Logic (abstract)

14:00-15:30 Session 3D (ALCS)

Chair: Carles Noguera

14:00	Tomasz Kowalski Representations for Ramsey Relation Algebras (abstract)
14:30	Luca Spada and Vincenzo Marra An Isomorphism Criterion for Colimits of Sequences of Finitely Presented Objects (abstract)
15:00	Petr Cintula and Carles Noguera A Completeness Theorem for Two-Layer Modal Logics (abstract)

15:30-16:00Coffee Break

16:00-17:30 Session 4A (IWIL)

Chair: Geoff Sutcliffe

16:00	Daniel Méry, Didier Galmiche and Jean-René Courtault An Interactive Prover for Bi-Intuitionistic Logic (abstract)
16:30	Ronan Saillard and Olivier Hermant Towards Explicit Rewrite Rules in the Lambda-Pi Calculus Modulo (abstract)
17:00	David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand and Olivier Hermant 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)

Chair: James Raftery

16:00	Willem Conradie and Andrew Craig Algorithmic-Algebraic Canonicity for Mu-Calculi (abstract)
16:30	Christoph Benzmueller Cut-free Calculi for Challenge Logics in a Lazy Way (abstract)

16:00-17:00 Session 4C (LRCM)

Chair: Katarina Britz

16:00	Nasubo Ongoma and C. Maria Keet Toward Representing Attributes in Temporal Conceptual Data Models (abstract)
16:30	Giovanni Casini and Alessandro Mosca 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)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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 (LPAR)

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)