default search action
5th IJCAR 2010: Edinburgh, UK
- Jürgen Giesl
, Reiner Hähnle
Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings. Lecture Notes in Computer Science 6173, Springer 2010, ISBN 978-3-642-14202-4
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, Jana Dunfield:
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). 15-21 - Silvio Ghilardi
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
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
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
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
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
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 S. 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
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. 384-399
Invited Talk
- Leonardo Mendonça de Moura, Nikolaj S. 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
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
On the Saturation of YAGO. 441-456
Description Logic II
- Birte Glimm, Ian Horrocks
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
Decreasing Diagrams and Relative Termination. 487-501 - Friedrich Neurauter, Aart Middeldorp
Monotonicity Criteria for Polynomial Interpretations over the Naturals. 502-517 - Sarah Winkler
Termination Tools in Ordered Completion. 518-532
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-22 19:08 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: