5. IJCAR (CADE, FroCoS, TABLEAUX, FTP) 2010: Edinburgh, UK

Logical Frameworks and Combination of Systems

• Anders Schack-Nielsen, Carsten Schürmann:
  Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus. 1-14
  
• Brigitte Pientka, Joshua Dunfield:
  Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). 15-21
  
• Silvio Ghilardi, Silvio Ranise:
  MCMT: A Model Checker Modulo Theories. 22-29
  
• Carsten Ihlemann, Viorica Sofronie-Stokkermans:
  On Hierarchical Reasoning in Combinations of Theories. 30-45
  

Description Logic I

• Rajeev Goré, Clemens Kupke, Dirk Pattinson, Lutz Schröder:
  Global Caching for Coalgebraic Description Logics. 46-60
  
• Despoina Magka, Yevgeny Kazakov, Ian Horrocks:
  Tractable Extensions of the Description Logic EL with Numerical Datatypes. 61-75
  

Higher-Order Logic

• Julian Backes, Chad E. Brown:
  Analytic Tableaux for Higher-Order Logic with Choice. 76-90
  
• Jasmin Christian Blanchette, Alexander Krauss:
  Monotonicity Inference for Higher-Order Formulas. 91-106
  
• Sascha Böhme, Tobias Nipkow:
  Sledgehammer: Judgement Day. 107-121
  

Invited Talk

• Johan van Benthem:
  Logic between Expressivity and Complexity. 122-126
  

Verification

• Ali Ayad, Claude Marché:
  Multi-Prover Verification of Floating-Point Programs. 127-141
  
• Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
  Verifying Safety Properties with the TLA+ Proof System. 142-148
  
• Ruzica Piskac, Viktor Kuncak:
  MUNCH - Automated Reasoner for Sets and Multisets. 149-155
  
• Elena Sherman, Brady J. Garvin, Matthew B. Dwyer:
  A Slice-Based Decision Procedure for Type-Based Partial Orders. 156-170
  
• Viorica Sofronie-Stokkermans:
  Hierarchical Reasoning for the Verification of Parametric Systems. 171-187
  

First-Order Logic

• Krystof Hoder, Laura Kovács, Andrei Voronkov:
  Interpolation and Symbol Elimination in Vampire. 188-195
  
• Konstantin Korovin, Christoph Sticksel:
  iProver-Eq: An Instantiation-Based Theorem Prover with Equality. 196-202
  
• Hans de Nivelle:
  Classical Logic with Partial Functions. 203-217
  

Non-Classical Logic

• Christoph Beierle, Marc Finthammer, Gabriele Kern-Isberner, Matthias Thimm:
  Automated Reasoning for Relational Probabilistic Knowledge Representation. 218-224
  
• Rajeev Goré, Florian Widmann:
  Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse. 225-239
  
• Mark Kaminski, Gert Smolka:
  Terminating Tableaux for Hybrid Logic with Eventualities. 240-254
  
• Marta Cialdea Mayer, Serenella Cerrito:
  Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic. 255-262
  

Induction

• Markus Aderhold:
  Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion. 263-277
  
• David Baelde, Dale Miller, Zachary Snow:
  Focused Inductive Theorem Proving. 278-292
  

Decision Procedures

• Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
  A Decidable Class of Nested Iterated Schemata. 293-308
  
• Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
  RegSTAB: A SAT Solver for Propositional Schemata. 309-315
  
• Nikolaj Bjørner:
  Linear Quantifier Elimination as an Abstract Decision Procedure. 316-330
  
• Oliver Friedmann, Markus Latte, Martin Lange:
  A Decision Procedure for CTL^* Based on Tableaux and Automata. 331-345
  
• Filip Maric, Predrag Janicic:
  URBiVA: Uniform Reduction to Bit-Vector Arithmetic. 346-352
  

Keynote Talk

• Deepak Kapur:
  Induction, Invariants, and Abstraction. 353
  

Arithmetic

• Jonathan Alexander Abourbih, Luke Blaney, Alan Bundy, Fiona McNeill:
  A Single-Significant-Digit Calculus for Semi-Automated Guesstimation. 354-368
  
• Hicham Bensaid, Ricardo Caferra, Nicolas Peltier:
  Perfect Discrimination Graphs: Indexing Terms with Integer Exponents. 369-383
  
• Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl:
  An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. 384-399
  

Invited Talk

• Leonardo Mendonça de Moura, Nikolaj Bjørner:
  Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. 400-411
  

Applications

• Vincent Cheval, Hubert Comon-Lundh, Stéphanie Delaune:
  Automating Security Analysis: Symbolic Equivalence of Constraint Systems. 412-426
  
• Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo:
  System Description: The Proof Transformation System CERES. 427-433
  
• Marcos Cramer, Peter Koepke, Daniel Kühlwein, Bernhard Schröder:
  Premise Selection in the Naproche System. 434-440
  
• Martin Suda, Christoph Weidenbach, Patrick Wischnewski:
  On the Saturation of YAGO. 441-456
  

Description Logic II

• Birte Glimm, Ian Horrocks, Boris Motik:
  Optimized Description Logic Reasoning via Core Blocking. 457-471
  
• Yevgeny Kazakov:
  An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ. 472-486
  

Termination

• Nao Hirokawa, Aart Middeldorp:
  Decreasing Diagrams and Relative Termination. 487-501
  
• Friedrich Neurauter, Aart Middeldorp, Harald Zankl:
  Monotonicity Criteria for Polynomial Interpretations over the Naturals. 502-517
  
• Sarah Winkler, Aart Middeldorp:
  Termination Tools in Ordered Completion. 518-532
  

Last update Wed May 22 01:09:56 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page