default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID19th CADE 2003: Miami Beach, Florida, USA
- Franz Baader:
Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings. Lecture Notes in Computer Science 2741, Springer 2003, ISBN 3-540-40559-3
Invited Talk
- Edmund M. Clarke:
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. 1
Session 2
- José Meseguer, Miguel Palomino, Narciso Martí-Oliet:
Equational Abstractions. 2-16 - Jürgen Giesl
, Deepak Kapur:
Deciding Inductive Validity of Equations. 17-31 - Nao Hirokawa, Aart Middeldorp:
Automating the Dependency Pair Method. 32-46 - Konstantin Korovin, Andrei Voronkov:
An AC-Compatible Knuth-Bendix Order. 47-59
Session 3
- Carsten Lutz, Ulrike Sattler, Lidia Tendera:
The Complexity of Finite Model Reasoning in Description Logics. 60-74 - Guoqiang Pan, Moshe Y. Vardi:
Optimizing a BDD-Based Modal Solver. 75-89 - Jan Hladik, Ulrike Sattler:
A Translation of Looping Alternating Automata into Description Logics. 90-105
Session 4
- Karl Crary, Susmit Sarkar:
Foundational Certified Code in a Metalogical Framework. 106-120 - Farhad Mehta, Tobias Nipkow:
Proving Pointer Programs in Higher-Order Logic. 121-135 - Dimitri Hendriks, Vincent van Oostrom:
adbmal. 136-150 - Aaron Stump:
Subset Types and Partial Functions. 151-165
Session 5
- Greg Nelson:
Reasoning about Quantifiers by Matching in the E-graph. 166
Session 6
- Sumit Gulwani, George C. Necula:
A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols. 167-181 - Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann:
Superposition Modulo a Shostak Theory. 182-196 - Sava Krstic, Sylvain Conchon:
Canonization for Disjoint Unions of Theories. 197-211 - Christophe Ringeissen:
Matching in a Class of Combined Non-disjoint Theories. 212-227
Session 7
- Johan G. F. Belinfante:
Reasoning about Iteration in Gödel's Class Theory. 228-242 - Panagiotis Manolios, Daron Vroon:
Algorithms for Ordinal Arithmetic. 243-257 - Arjeh M. Cohen, Scott H. Murray, Martin Pollet, Volker Sorge:
Certifying Solutions to Permutation Group Problems. 258-273
System Descriptions
- Ullrich Hustadt, Boris Konev:
TRP++2.0: A Temporal Resolution Prover. 274-278 - Lucas Dixon, Jacques D. Fleuriot:
IsaPlanner: A Prototype Proof Planner in Isabelle. 279-283 - Peter Baumgartner, Ulrich Furbach, Margret Groß-Hardt, Alex Sinner:
'Living Book': -'Deduction', 'Slicing', 'Interaction'. 284-288 - Simon Colton, Sophie Huczynska:
The Homer System. 289-294
CASC-19 Results
- Geoff Sutcliffe, Christian B. Suttner:
The CADE-19 ATP System Competition. 295-296
Invited Talk
- Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen:
Proof Search and Proof Check for Equational and Inductive Theorems. 297-316
System Descriptions
- Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, Hendrik Spies:
The New WALDMEISTER Loop at Work. 317-321 - Christoph Walther, Stephan Schweitzer:
About VeriFun. 322-327 - Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth:
How to Prove Inductive Theorems? QUODLIBET! 328-333
Invited Talk
- Anthony G. Cohn:
Reasoning about Qualitative Representations of Space and Time. 334
Session 13
- Harald Ganzinger, Jürgen Stuber:
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. 335-349 - Peter Baumgartner, Cesare Tinelli:
The Model Evolution Calculus. 350-364 - Hans de Nivelle:
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. 365-379 - Alexandre Riazanov, Andrei Voronkov:
Efficient Instance Retrieval with Standard and Relational Path Indexing. 380-396
Session 14
- Anatoli Degtyarev, Michael Fisher, Boris Konev:
Monodic Temporal Resolution. 397-411 - Renate A. Schmidt, Ullrich Hustadt:
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. 412-426 - Christopher Lynch:
Schematic Saturation for Decision and Unification Problems. 427-441
Session 15
- Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch:
Unification Modulo ACU I Plus Homomorphisms/Distributivity. 442-457 - Venkatesh Choppella, Christopher T. Haynes:
Source-Tracking Unification. 458-472 - Brigitte Pientka, Frank Pfenning:
Optimizing Higher-Order Pattern Unification. 473-487 - Manfred Schmidt-Schauß:
Decidability of Arity-Bounded Higher-Order Matching. 488-502
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 2026-04-26 00:06 CEST 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:
