6. FTP 2004: Cork, County Cork, Ireland

David A. Basin, Michaël Rusinowitch (Eds.): Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings. Lecture Notes in Computer Science 3097 Springer 2004, ISBN 3-540-22345-2

Rewriting

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

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

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

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

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

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

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

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

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

Geoff Sutcliffe, Christian B. Suttner:
The CADE ATP System Competition. 490-491

Last update Fri May 24 00:29:28 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page