2. IJCAR / CADE / 13. TABLEAUX / 5. FroCoS / 6. FTP 2004: Cork, County Cork, Ireland

Rewriting

• José Meseguer, Grigore Rosu:
  Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. 1-44
  Electronic Edition (link) BibTeX
• Bernd Löchner:
  A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting. 45-59
  Electronic Edition (link) BibTeX
• Alexandre Riazanov, Andrei Voronkov:
  Efficient Checking of Term Ordering Constraints. 60-74
  Electronic Edition (link) BibTeX
• René Thiemann, Jürgen Giesl, Peter Schneider-Kamp:
  Improved Modular Termination Proofs Using Dependency Pairs. 75-90
  Electronic Edition (link) BibTeX
• Guillem Godoy, Ashish Tiwari:
  Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure. 91-106
  Electronic Edition (link) BibTeX

Saturation-Based Theorem Proving

• Miquel Bofill, Albert Rubio:
  Redundancy Notions for Paramodulation with Non-monotonic Orderings. 107-121
  Electronic Edition (link) BibTeX
• Yevgeny Kazakov, Hans de Nivelle:
  A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards. 122-136
  Electronic Edition (link) BibTeX
• Graham Steel, Alan Bundy, Monika Maidl:
  Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures. 137-151
  Electronic Edition (link) BibTeX

Combination Techniques

• Ting Zhang, Henny B. Sipma, Zohar Manna:
  Decision Procedures for Recursive Data Structures with Integer Constraints. 152-167
  Electronic Edition (link) BibTeX
• Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann:
  Modular Proof Systems for Partial Functions with Weak Equality. 168-182
  Electronic Edition (link) BibTeX
• Franz Baader, Silvio Ghilardi, Cesare Tinelli:
  A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics. 183-197
  Electronic Edition (link) BibTeX

Verification and Systems

• Ewen Denney, Bernd Fischer, Johann Schumann:
  Using Automated Theorem Provers to Certify Auto-generated Aerospace Software. 198-212
  Electronic Edition (link) BibTeX
• Filip Maric, Predrag Janicic:
  argo-lib: A Generic Platform for Decision Procedures. 213-217
  Electronic Edition (link) BibTeX
• Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar:
  The ICS Decision Procedures for Embedded Deduction. 218-222
  Electronic Edition (link) BibTeX
• Stephan Schulz:
  System Description: E 0.81. 223-228
  Electronic Edition (link) BibTeX

Reasoning with Finite Structure

• Georg Gottlob:
  Second-Order Logic over Finite Structures - Report on a Research Programme. 229-243
  Electronic Edition (link) BibTeX
• Àngel J. Gil, Miki Hermann, Gernot Salzer, Bruno Zanuttini:
  Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains: Extended Abstract. 244-258
  Electronic Edition (link) BibTeX

Tableaux and Non-classical Logics

• Carsten Lutz, Dirk Walther:
  PDL with Negation of Atomic Programs. 259-273
  Electronic Edition (link) BibTeX
• Dominique Larchey-Wendling:
  Counter-Model Search in Gödel-Dummett Logics. 274-288
  Electronic Edition (link) BibTeX
• Reinhold Letz, Gernot Stenz:
  Generalised Handling of Variables in Disconnection Tableaux. 289-306
  Electronic Edition (link) BibTeX

Applications and Systems

• Tanel Tammet:
  Chain Resolution for the Semantic Web. 307-320
  Electronic Edition (link) BibTeX
• Anni-Yasmin Turhan, Christian Kissig:
  Sonic - Non-standard Inferences Go OilEd. 321-325
  Electronic Edition (link) BibTeX
• Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov:
  TeMP: A Temporal Monodic Prover. 326-330
  Electronic Edition (link) BibTeX
• Daniel Winterstein, Alan Bundy, Corin A. Gurr:
  Dr.Doodle: A Diagrammatic Theorem Prover. 331-335
  Electronic Edition (link) BibTeX

Computer Mathematics

• Volker Weispfenning:
  Solving Constraints by Elimination Methods. 336-341
  Electronic Edition (link) BibTeX
• K. Subramani:
  Analyzing Selected Quantified Integer Programs. 342-356
  Electronic Edition (link) BibTeX

Interactive Theorem Proving

• Jeremy Avigad, Kevin Donnelly:
  Formalizing O Notation in Isabelle/HOL. 357-371
  Electronic Edition (link) BibTeX
• Jia Meng, Lawrence C. Paulson:
  Experiments on Supporting Interactive Proof Using Resolution. 372-384
  Electronic Edition (link) BibTeX
• Gilles Barthe, Jan Cederquist, Sabrina Tarento:
  A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. 385-399
  Electronic Edition (link) BibTeX

Combinatorial Reasoning

• Simon Colton, Andreas Meier, Volker Sorge, Roy L. McCasland:
  Automatic Generation of Classification Theorems for Finite Algebras. 400-414
  Electronic Edition (link) BibTeX
• Jürgen Avenhaus:
  Efficient Algorithms for Computing Modulo Permutation Theories. 415-429
  Electronic Edition (link) BibTeX
• Thierry Boy de la Tour, Mnacho Echenim:
  Overlapping Leaf Permutative Equations. 430-444
  Electronic Edition (link) BibTeX

Higher-Order Reasoning

• Richard Bonichon:
  TaMeD: A Tableau Method for Deduction Modulo. 445-459
  Electronic Edition (link) BibTeX
• Michael Beeson:
  Lambda Logic. 460-474
  Electronic Edition (link) BibTeX
• William M. Farmer:
  Formalizing Undefinedness Arising in Calculus. 475-489
  Electronic Edition (link) BibTeX

Competition

• Geoff Sutcliffe, Christian B. Suttner:
  The CADE ATP System Competition. 490-491
  Electronic Edition (link) BibTeX