IJCAR 2010 Accepted Papers

Monotonicity Inference for Higher-Order Formulas
Sledgehammer: Judgement Day
Decreasing Diagrams and Relative Termination
MCMT: A Model Checker Modulo Theories
A Single-Significant-Digit Calculus for Semi-Automated Guesstimation
Analytic Tableaux for Higher-Order Logic with Choice
URBiVA: Uniform Reduction to Bit-Vector Arithmetic
Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion
Optimal Tableaux for Propositional Dynamic Logic with Converse
Termination Tools in Ordered Completion
Monotonicity Criteria for Polynomial Interpretations over the Naturals
Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
Multi-Prover Verification of Floating-Point Programs
Verifying Safety Properties With the TLA+ Proof System
Terminating Tableaux for Hybrid Logic with Eventualities
Tractable Extensions of the Description Logic EL with Numerical Datatypes
Perfect discrimination graphs: indexing terms with integer exponents
RegSTAB: a SAT-Solver for Propositional Schemata
Automated Reasoning for Relational Probabilistic Knowledge Representation
Symbol Elimination and Interpolation in Vampire
A Decidable Class of Nested Iterated Schemata
Focused Inductive Theorem Proving
Herod and Pilate: two tableau provers for basic hybrid logic
Automating security analysis: symbolic equivalence of constraint systems
A Decision Procedure for CTL* Based on Tableaux and Automata
iProver-Eq: An Instantiation-based Theorem Prover with Equality
On efficient reasoning in combinations of theories
Classical Logic with Partial Functions
MUNCH - Automated Reasoner for Sets and Multisets
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
Global Caching for Coalgebraic Description Logics
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
A Slice-based Decision Procedure for Type-based Partial Orders
Hierarchical reasoning for the verification of parametric systems
Linear Quantifier Elimination as an Abstract Decision Procedure
Optimized Description Logic Reasoning via Core Blocking
An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ