default search action
2nd IJCAR 2004: Cork, County Cork, Ireland
- David A. Basin, Michaël Rusinowitch:
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
Saturation-Based Theorem Proving
- 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
Combination Techniques
- 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
Verification and Systems
- 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
Reasoning with Finite Structure
- 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
Tableaux and Non-classical Logics
- 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
Applications and Systems
- 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
Computer Mathematics
- Volker Weispfenning:
Solving Constraints by Elimination Methods. 336-341 - K. Subramani:
Analyzing Selected Quantified Integer Programs. 342-356
Interactive Theorem Proving
- 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
Combinatorial Reasoning
- 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
Higher-Order Reasoning
- Richard Bonichon:
TaMeD: A Tableau Method for Deduction Modulo. 445-459 - Michael Beeson:
Lambda Logic. 460-474 - William M. Farmer:
Formalizing Undefinedness Arising in Calculus. 475-489
Competition
- Geoff Sutcliffe, Christian B. Suttner:
The CADE ATP System Competition. 490-491
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.