4. IJCAR (CADE, FroCoS, TABLEAUX, FTP) 2008: Sydney, NSW, Australia

Invited Talk

• Aarti Gupta:
  Software Verification: Roles and Challenges for Automatic Decision Procedures. 1
  

Specific Theories

• Guillaume Melquiond:
  Proving Bounds on Real-Valued Functions with Computations. 2-17
  
• Tobias Nipkow:
  Linear Quantifier Elimination. 18-33
  
• Marius Bozga, Radu Iosif, Swann Perarnau:
  Quantitative Separation Logic and Programs with Lists. 34-49
  
• Peter Höfner, Georg Struth:
  On Automating the Calculus of Relations. 50-66
  

Automated Verification

• Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli:
  Towards SMT Model Checking of Array-Based Systems. 67-82
  
• Gilles Barthe, Benjamin Grégoire, Mariela Pavlova:
  Preservation of Proof Obligations from Java to the Java Virtual Machine. 83-99
  
• Ádám Darvas, Farhad Mehta, Arsenii Rudich:
  Efficient Well-Definedness Checking. 100-115
  

Protocol Verification

• Steve Kremer, Antoine Mercier, Ralf Treinen:
  Proving Group Protocols Secure Against Eavesdroppers. 116-131
  

System Descriptions 1

• Martin Avanzini, Georg Moser, Andreas Schnabl:
  Automated Implicit Computational Complexity Analysis (System Description). 132-138
  
• Ulrich Furbach, Ingo Glöckner, Hermann Helbig, Björn Pelzer:
  LogAnswer - A Deduction-Based Question Answering System (System Description). 139-146
  
• Christoph Beierle, Gabriele Kern-Isberner, Nicole Koch:
  A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description). 147-153
  
• Andrew Gacek:
  The Abella Interactive Theorem Prover (System Description). 154-161
  
• Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke:
  LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). 162-170
  
• André Platzer, Jan-David Quesel:
  KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). 171-178
  

Invited Talk

• Carsten Lutz:
  The Complexity of Conjunctive Query Answering in Expressive Description Logics. 179-193
  

Modal Logics

• Renate A. Schmidt, Dmitry Tishkovsky:
  A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. 194-209
  
• Mark Kaminski, Gert Smolka:
  Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse. 210-225
  

Description Logics

• Franz Baader, Rafael Peñaloza:
  Automata-Based Axiom Pinpointing. 226-241
  
• Boris Motik, Ian Horrocks:
  Individual Reuse in Description Logic Reasoning. 242-258
  
• Boris Konev, Dirk Walther, Frank Wolter:
  The Logical Difference Problem for Description Logic Terminologies. 259-274
  

System Descriptions 2

• Laura Kovács:
  Aligator: A Mathematica Package for Invariant Generation (System Description). 275-282
  
• Jens Otten:
  leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions). 283-291
  
• Konstantin Korovin:
  iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). 292-298
  
• Rajeev Goré, Linda Postniece:
  An Experimental Evaluation of Global Caching for (System Description). 299-305
  
• Haruhiko Sato, Sarah Winkler, Masahito Kurihara, Aart Middeldorp:
  Multi-completion with Termination Tools (System Description). 306-312
  
• Francisco Durán, Salvador Lucas, José Meseguer:
  MTT: The Maude Termination Tool (System Description). 313-319
  
• Anders Schack-Nielsen, Carsten Schürmann:
  Celf - A Logical Framework for Deductive and Concurrent Systems (System Description). 320-326
  

Invited Talk

• Nachum Dershowitz:
  Canonicity! 327-331
  

Equational Theories

• Thierry Boy de la Tour, Mnacho Echenim, Paliath Narendran:
  Unification and Matching Modulo Leaf-Permutative Equational Presentations. 332-347
  
• Vincent van Oostrom:
  Modularity of Confluence. 348-363
  
• Nao Hirokawa, Georg Moser:
  Automated Complexity Analysis Based on the Dependency Pair Method. 364-379
  
• Maria Paola Bonacina, Nachum Dershowitz:
  Canonical Inference for Implicational Systems. 380-395
  

Invited Talk

• Hubert Comon-Lundh:
  Challenges in the Automated Verification of Security Protocols. 396-409
  

Theorem Proving 1

• Leonardo Mendonça de Moura, Nikolaj Bjørner:
  Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. 410-425
  
• Juan Antonio Navarro Pérez, Andrei Voronkov:
  Proof Systems for Effectively Propositional Logic. 426-440
  
• Josef Urban, Geoff Sutcliffe, Petr Pudlák, Jirí Vyskocil:
  MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance. 441-456
  

CASC

• Geoff Sutcliffe:
  CASC-J4 The 4th IJCAR ATP System Competition. 457-458
  

Theorem Proving 2

• Arnaud Fietzke, Christoph Weidenbach:
  Labelled Splitting. 459-474
  
• Leonardo Mendonça de Moura, Nikolaj Bjørner:
  Engineering DPLL(T) + Saturation. 475-490
  
• Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe:
  THF0 - The Core of the TPTP Language for Higher-Order Logic. 491-506
  

Logical Frameworks

• Vivek Nigam, Dale Miller:
  Focusing in Linear Meta-logic. 507-522
  

Tree Automata

• Benoît Boyer, Thomas Genet, Thomas P. Jensen:
  Certifying a Tree Automata Completion Checker. 523-538
  
• Adel Bouhoula, Florent Jacquemard:
  Automated Induction with Constrained Tree Automata. 539-554