Jürgen Giesl, Reiner Hähnle
Proceedings of the Fifth International Joint Conference on Automated Reasoning
IJCAR, 2010.

@proceedings{IJCAR-2010,
	address       = "Edinburgh, Scotland, United Kingdom",
	doi           = "10.1007/978-3-642-14203-1",
	editor        = "Jürgen Giesl and Reiner Hähnle",
	isbn          = "978-3-642-14202-4",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fifth International Joint Conference on Automated Reasoning}",
	volume        = 6173,
	year          = 2010,
}

Contents (43 items)

10 ×#logic
7 ×#named
6 ×#reasoning
5 ×#automation
5 ×#proving
3 ×#higher-order
3 ×#induction
3 ×#verification
2 ×#axiom
2 ×#calculus

IJCAR-2010-Schack-NielsenS #linear #λ-calculus

Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus (ASN, CS), pp. 1–14.

IJCAR-2010-PientkaD #deduction #framework #named #programming #reasoning

Beluga: A Framework for Programming and Reasoning with Deductive Systems (BP, JD), pp. 15–21.

IJCAR-2010-GhilardiR #model checking #modulo theories #named

MCMT: A Model Checker Modulo Theories (SG, SR), pp. 22–29.

IJCAR-2010-IhlemannS #on the #reasoning

On Hierarchical Reasoning in Combinations of Theories (CI, VSS), pp. 30–45.

IJCAR-2010-GoreKPS #algebra #logic

Global Caching for Coalgebraic Description Logics (RG, CK, DP, LS), pp. 46–60.

IJCAR-2010-MagkaKH #data type #logic

Tractable Extensions of the Description Logic EL with Numerical Datatypes (DM, YK, IH), pp. 61–75.

IJCAR-2010-BackesB #higher-order #logic

Analytic Tableaux for Higher-Order Logic with Choice (JB, CEB), pp. 76–90.

IJCAR-2010-BlanchetteK #higher-order

Monotonicity Inference for Higher-Order Formulas (JCB, AK), pp. 91–106.

IJCAR-2010-BohmeN #named

Sledgehammer: Judgement Day (SB, TN), pp. 107–121.

IJCAR-2010-Benthem #complexity #logic

Logic between Expressivity and Complexity (JvB), pp. 122–126.

IJCAR-2010-AyadM #float #multi #source code #verification

Multi-Prover Verification of Floating-Point Programs (AA, CM), pp. 127–141.

IJCAR-2010-ChaudhuriDLM #proving #safety #verification

Verifying Safety Properties with the TLA+ Proof System (KC, DD, LL, SM), pp. 142–148.

IJCAR-2010-PiskacK #automation #multi #named #set

MUNCH — Automated Reasoner for Sets and Multisets (RP, VK), pp. 149–155.

IJCAR-2010-ShermanGD #partial order #type system

A Slice-Based Decision Procedure for Type-Based Partial Orders (ES, BJG, MBD), pp. 156–170.

IJCAR-2010-Sofronie-Stokkermans #parametricity #reasoning #verification

Hierarchical Reasoning for the Verification of Parametric Systems (VSS), pp. 171–187.

IJCAR-2010-HoderKV

Interpolation and Symbol Elimination in Vampire (KH, LK, AV), pp. 188–195.

IJCAR-2010-KorovinS #named #proving #similarity #theorem proving

iProver-Eq: An Instantiation-Based Theorem Prover with Equality (KK, CS), pp. 196–202.

IJCAR-2010-Nivelle #logic

Classical Logic with Partial Functions (HdN), pp. 203–217.

IJCAR-2010-BeierleFKT #automation #information management #probability #reasoning #relational #representation

Automated Reasoning for Relational Probabilistic Knowledge Representation (CB, MF, GKI, MT), pp. 218–224.

IJCAR-2010-GoreW #logic

Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse (RG, FW), pp. 225–239.

IJCAR-2010-KaminskiS #hybrid #logic

Terminating Tableaux for Hybrid Logic with Eventualities (MK, GS), pp. 240–254.

IJCAR-2010-MayerC #hybrid #logic #proving

Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic (MCM, SC), pp. 255–262.

IJCAR-2010-Aderhold #automation #axiom #higher-order #induction #recursion #source code #synthesis

Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion (MA), pp. 263–277.

IJCAR-2010-BaeldeMS #induction #proving #theorem proving

Focused Inductive Theorem Proving (DB, DM, ZS), pp. 278–292.

IJCAR-2010-AravantinosCP #decidability

A Decidable Class of Nested Iterated Schemata (VA, RC, NP), pp. 293–308.

IJCAR-2010-AravantinosCP10a #named #satisfiability

RegSTAB: A SAT Solver for Propositional Schemata (VA, RC, NP), pp. 309–315.

IJCAR-2010-Bjorner #linear #quantifier

Linear Quantifier Elimination as an Abstract Decision Procedure (NB), pp. 316–330.

IJCAR-2010-FriedmannLL #automaton

A Decision Procedure for CTL* Based on Tableaux and Automata (OF, ML, ML), pp. 331–345.

IJCAR-2010-MaricJ #named #reduction

URBiVA: Uniform Reduction to Bit-Vector Arithmetic (FM, PJ), pp. 346–352.

IJCAR-2010-Kapur #abstraction #induction #invariant

Induction, Invariants, and Abstraction (DK), p. 353.

IJCAR-2010-AbourbihBBM #automation #calculus

A Single-Significant-Digit Calculus for Semi-Automated Guesstimation (JAA, LB, AB, FM), pp. 354–368.

IJCAR-2010-BensaidCP #graph #integer

Perfect Discrimination Graphs: Indexing Terms with Integer Exponents (HB, RC, NP), pp. 369–383.

IJCAR-2010-BrilloutKRW #calculus #quantifier

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic (AB, DK, PR, TW), pp. 384–399.

IJCAR-2010-MouraB #debugging #development #reasoning

Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development (LMdM, NB), pp. 400–411.

IJCAR-2010-ChevalCD #analysis #automation #constraints #equivalence #security

Automating Security Analysis: Symbolic Equivalence of Constraint Systems (VC, HCL, SD), pp. 412–426.

IJCAR-2010-DunchevLLWP #proving

System Description: The Proof Transformation System CERES (TD, AL, TL, DW, BWP), pp. 427–433.

IJCAR-2010-CramerKKS

Premise Selection in the Naproche System (MC, PK, DK, BS), pp. 434–440.

IJCAR-2010-SudaWW #on the

On the Saturation of YAGO (MS, CW, PW), pp. 441–456.

IJCAR-2010-GlimmHM #logic #reasoning

Optimized Description Logic Reasoning via Core Blocking (BG, IH, BM), pp. 457–471.

IJCAR-2010-Kazakov #axiom #logic

An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ (YK), pp. 472–486.

IJCAR-2010-HirokawaM #diagrams #termination

Decreasing Diagrams and Relative Termination (NH, AM), pp. 487–501.

IJCAR-2010-NeurauterMZ #polynomial

Monotonicity Criteria for Polynomial Interpretations over the Naturals (FN, AM, HZ), pp. 502–517.

IJCAR-2010-WinklerM #order #termination #tool support

Termination Tools in Ordered Completion (SW, AM), pp. 518–532.