IJCAR 2012 - The 6th International Joint Conference on Automated Reasoning

June 26
• Yuri Matiyasevich: Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics

• François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout and Guillaume Melquiond: A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic

• Stephan Falke and Deepak Kapur: Rewriting Induction + Linear Arithmetic = Decision Procedure

• Dejan Jovanović and Leonardo De Moura: Solving Non-Linear Arithmetic

• Pierre-Cyrille Heam, Vincent Hugot and Olga Kouchnarenko: From Linear Temporal Logic Properties to Rewrite Propositions

• Markus Latte and Martin Lange: Branching Time? Pruning Time!

• Stéphane Demri, Amit Kumar Dhar and Arnaud Sangnier: Taming Past LTL and Flat Counter Systems

• Jan-David Quesel and Andre Platzer: Playing Hybrid Games with KeYmaera

• Matthias Baaz, Ori Lahav and Anna Zamansky: Effective Finite-valued Semantics for Labelled Calculi

• Rajeev Gore and Jimmy Thomson: BDD-based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics

June 27
• Robert Nieuwenhuis: SAT and SMT Are Still Resolution: Questions and Challenges

• Sicun Gao, Jeremy Avigad and Edmund Clarke: Delta-Complete Decision Procedures for Satisfiability over the Reals

• Andrej Spielmann and Viktor Kuncak: Synthesis for Unbounded Bitvector Arithmetic

• Roberto Sebastiani and Silvia Tomasi: Optimization in SMT with LA(Q) Cost Functions

• Andrew Marshall and Paliath Narendran: A New Algorithm for Unification Modulo One-Sided Distributivity

• Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran and Michael Rusinowitch: Unification modulo Synchronous Distributivity

• Franz Baader, Stefan Borgwardt and Barbara Morawska: SAT-Encoding of Unification in ELHR+ w.r.t. Cycle-Restricted Ontologies

• Alwen Tiu: Stratification in Logics of Definitions

• Roberto Bruttomesso, Silvio Ghilardi and Silvio Ranise: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation

• Pascal Fontaine, Stephan Merz and Christoph Weidenbach: Combination of disjoint theories: beyond decidability

• Afternoon Lecture by Peter Andrews

June 28
• Nicole Schweikardt: Querying graph structured data

• Stefan Borgwardt, Felix Distel and Rafael Peñaloza: How Fuzzy is my Fuzzy Description Logic?

• Andreas Steigmiller, Thorsten Liebig and Birte Glimm: Extended Caching, Backjumping and Merging for Expressive Description Logics

• Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Geneves and Nabil Layaïda: SPARQL Query Containment under RDFS Entailment Regime

• Frank de Boer, Marcello Bonsangue and Jurriaan Rot: Automated Verification of Recursive Programs with Pointers

• Taus Brock-Nannestad and Carsten Schuermann: Truthful Monadic Abstractions

• Chad Brown: Satallax: An Automated Higher-Order Prover

• Thomas Raths and Jens Otten: The QMLTP Problem Library for First-order Modal Logics

• Matti Järvisalo, Marijn Heule and Armin Biere: Inprocessing Rules

• Daniel Kuehlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban and Tom Heskes: Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics

• Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel and Andrei Voronkov: EPR-based bounded model checking at word level

• Afternoon Lecture by Martin Davis

June 29
• Nikolaj Bjorner: Taking Satisfiability to the Next Level with Z3

• Đurica Nikolić and Fausto Spoto: Reachability Analysis of Program Variables

• Conrad Rau, David Sabel and Manfred Schmidt-Schauss: Correctness of Program Transformations as a Termination Problem

• Fabian Emmes, Tim Enger and Jürgen Giesl: Proving Non-Looping Non-Termination Automatically

• Jürgen Giesl: Results from Termination Competition

• Mélanie Jacquel, Karim Berkani, David Delahaye and Catherine Dubois: Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover

• Thomas Sternagel and Harald Zankl: KBCV – Knuth-Bendix Completion Visualizer

• Stephan Schulz: Fingerprint Indexing for Paramodulation and Rewriting

• Boris Konev, Michel Ludwig and Frank Wolter: Logical Difference Computation with CEX 2.5

• Matej Urbas and Mateja Jamnik: Diabelli: A heterogeneous reasoning framework

• Martin Suda and Christoph Weidenbach: A PLTL-prover based on labelled superposition with partial model guidance

• Franz Baader, Julian Mendez and Barbara Morawska: UEL: Unification Solver for the Description Logic EL, System Description

• Simon Foster and Georg Struth: Automated Analysis of Regular Algebra

• Mnacho Echenim and Nicolas Peltier: A Calculus for Generating Ground Explanations

• Stephanie Delaune, Steve Kremer and Daniel Pasaila: Security protocols, constraint systems, and group theories

• Afternoon Lecture by John Alan Robinson