Invited Talks

• 
  Nikolaj Bjørner: Taking Satisfiability to the Next Level with Z3 - (Abstract). 1-8
• 
  Yuri Matiyasevich: Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics. 9
• 
  Robert Nieuwenhuis: SAT and SMT Are Still Resolution: Questions and Challenges. 10-13

Full Papers and System Descriptions

• 
  Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran, Michaël Rusinowitch: Unification Modulo Synchronous Distributivity. 14-29
• 
  Franz Baader, Stefan Borgwardt, Barbara Morawska: SAT Encoding of Unification in $\mathcal{ELH}_{{R}^+}$ w.r.t. Cycle-Restricted Ontologies. 30-44
• 
  Franz Baader, Julian Mendez, Barbara Morawska: UEL: Unification Solver for the Description Logic $\mathcal{EL}$ - System Description. 45-51
• 
  Matthias Baaz, Ori Lahav, Anna Zamansky: Effective Finite-Valued Semantics for Labelled Calculi. 52-66
• 
  François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond: A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. 67-81
• 
  Stefan Borgwardt, Felix Distel, Rafael Peñaloza: How Fuzzy Is My Fuzzy Description Logic? 82-96
• 
  Taus Brock-Nannestad, Carsten Schürmann: Truthful Monadic Abstractions. 97-110
• 
  Chad E. Brown: Satallax: An Automatic Higher-Order Prover. 111-117
• 
  Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. 118-133
• 
  Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Genevès, Nabil Layaïda: SPARQL Query Containment under RDFS Entailment Regime. 134-148
• 
  Frank S. de Boer, Marcello M. Bonsangue, Jurriaan Rot: Automated Verification of Recursive Programs with Pointers. 149-163
• 
  Stéphanie Delaune, Steve Kremer, Daniel Pasaila: Security Protocols, Constraint Systems, and Group Theories. 164-178
• 
  Stéphane Demri, Amit Kumar Dhar, Arnaud Sangnier: Taming Past LTL and Flat Counter Systems. 179-193
• 
  Mnacho Echenim, Nicolas Peltier: A Calculus for Generating Ground Explanations. 194-209
• 
  Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov: EPR-Based Bounded Model Checking at Word Level. 210-224
• 
  Fabian Emmes, Tim Enger, Jürgen Giesl: Proving Non-looping Non-termination Automatically. 225-240
• 
  Stephan Falke, Deepak Kapur: Rewriting Induction + Linear Arithmetic = Decision Procedure. 241-255
• 
  Pascal Fontaine, Stephan Merz, Christoph Weidenbach: Combination of Disjoint Theories: Beyond Decidability. 256-270
• 
  Simon Foster, Georg Struth: Automated Analysis of Regular Algebra. 271-285
• 
  Sicun Gao, Jeremy Avigad, Edmund M. Clarke: δ-Complete Decision Procedures for Satisfiability over the Reals. 286-300
• 
  Rajeev Goré, Jimmy Thomson: BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics. 301-315
• 
  Pierre-Cyrille Héam, Vincent Hugot, Olga Kouchnarenko: From Linear Temporal Logic Properties to Rewrite Propositions. 316-331
• 
  Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois: Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. 332-338
• 
  Dejan Jovanovic, Leonardo Mendonça de Moura: Solving Non-linear Arithmetic. 339-354
• 
  Matti Järvisalo, Marijn Heule, Armin Biere: Inprocessing Rules. 355-370
• 
  Boris Konev, Michel Ludwig, Frank Wolter: Logical Difference Computation with CEX2.5. 371-377
• 
  Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, Tom Heskes: Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics. 378-392
• 
  Markus Latte, Martin Lange: Branching Time? Pruning Time! 393-407
• 
  Andrew M. Marshall, Paliath Narendran: New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants. 408-422
• 
  Durica Nikolic, Fausto Spoto: Reachability Analysis of Program Variables. 423-438
• 
  Jan-David Quesel, André Platzer: Playing Hybrid Games with KeYmaera. 439-453
• 
  Thomas Raths, Jens Otten: The QMLTP Problem Library for First-Order Modal Logics. 454-461
• 
  Conrad Rau, David Sabel, Manfred Schmidt-Schauß: Correctness of Program Transformations as a Termination Problem. 462-476
• 
  Stephan Schulz: Fingerprint Indexing for Paramodulation and Rewriting. 477-483
• 
  Roberto Sebastiani, Silvia Tomasi: Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions. 484-498
• 
  Andrej Spielmann, Viktor Kuncak: Synthesis for Unbounded Bit-Vector Arithmetic. 499-513
• 
  Andreas Steigmiller, Thorsten Liebig, Birte Glimm: Extended Caching, Backjumping and Merging for Expressive Description Logics. 514-529
• 
  Thomas Sternagel, Harald Zankl: KBCV - Knuth-Bendix Completion Visualizer. 530-536
• 
  Martin Suda, Christoph Weidenbach: A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. 537-543
• 
  Alwen Tiu: Stratification in Logics of Definitions. 544-558
• 
  Matej Urbas, Mateja Jamnik: Diabelli: A Heterogeneous Proof System. 559-566

last updated on Thu May 23 03:07:00 2013 by the dblp team
data released under the ODC-BY 1.0 license
see also our legal information page