- 2003
- Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch:
Unification Modulo ACU I Plus Homomorphisms/Distributivity. CADE 2003: 442-457 - Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth:
How to Prove Inductive Theorems? QUODLIBET! CADE 2003: 328-333 - Peter Baumgartner, Ulrich Furbach, Margret Groß-Hardt, Alex Sinner:
'Living Book': -'Deduction', 'Slicing', 'Interaction'. CADE 2003: 284-288 - Peter Baumgartner, Cesare Tinelli:
The Model Evolution Calculus. CADE 2003: 350-364 - Johan G. F. Belinfante:
Reasoning about Iteration in Gödel's Class Theory. CADE 2003: 228-242 - Venkatesh Choppella, Christopher T. Haynes:
Source-Tracking Unification. CADE 2003: 458-472 - Edmund M. Clarke:
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. CADE 2003: 1 - Arjeh M. Cohen, Scott H. Murray, Martin Pollet, Volker Sorge:
Certifying Solutions to Permutation Group Problems. CADE 2003: 258-273 - Anthony G. Cohn:
Reasoning about Qualitative Representations of Space and Time. CADE 2003: 334 - Simon Colton, Sophie Huczynska:
The Homer System. CADE 2003: 289-294 - Karl Crary, Susmit Sarkar:
Foundational Certified Code in a Metalogical Framework. CADE 2003: 106-120 - Anatoli Degtyarev, Michael Fisher, Boris Konev:
Monodic Temporal Resolution. CADE 2003: 397-411 - Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen:
Proof Search and Proof Check for Equational and Inductive Theorems. CADE 2003: 297-316 - Lucas Dixon, Jacques D. Fleuriot:
IsaPlanner: A Prototype Proof Planner in Isabelle. CADE 2003: 279-283 - Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, Hendrik Spies:
The New WALDMEISTER Loop at Work. CADE 2003: 317-321 - Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann:
Superposition Modulo a Shostak Theory. CADE 2003: 182-196 - Harald Ganzinger, Jürgen Stuber:
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. CADE 2003: 335-349 - Jürgen Giesl, Deepak Kapur:
Deciding Inductive Validity of Equations. CADE 2003: 17-31 - Sumit Gulwani, George C. Necula:
A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols. CADE 2003: 167-181 - Dimitri Hendriks, Vincent van Oostrom:
adbmal. CADE 2003: 136-150 - Nao Hirokawa, Aart Middeldorp:
Automating the Dependency Pair Method. CADE 2003: 32-46 - Jan Hladik, Ulrike Sattler:
A Translation of Looping Alternating Automata into Description Logics. CADE 2003: 90-105 - Ullrich Hustadt, Boris Konev:
TRP++2.0: A Temporal Resolution Prover. CADE 2003: 274-278 - Konstantin Korovin, Andrei Voronkov:
An AC-Compatible Knuth-Bendix Order. CADE 2003: 47-59 - Sava Krstic, Sylvain Conchon:
Canonization for Disjoint Unions of Theories. CADE 2003: 197-211 - Carsten Lutz, Ulrike Sattler, Lidia Tendera:
The Complexity of Finite Model Reasoning in Description Logics. CADE 2003: 60-74 - Christopher Lynch:
Schematic Saturation for Decision and Unification Problems. CADE 2003: 427-441 - Panagiotis Manolios, Daron Vroon:
Algorithms for Ordinal Arithmetic. CADE 2003: 243-257 - Farhad Mehta, Tobias Nipkow:
Proving Pointer Programs in Higher-Order Logic. CADE 2003: 121-135 - José Meseguer, Miguel Palomino, Narciso Martí-Oliet:
Equational Abstractions. CADE 2003: 2-16