David A. Basin, Michaël Rusinowitch
Proceedings of the Second International Joint Conference on Automated Reasoning
IJCAR, 2004.

@proceedings{IJCAR-2004,
	address       = "Cork, Ireland",
	editor        = "David A. Basin and Michaël Rusinowitch",
	isbn          = "3-540-22345-2",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Second International Joint Conference on Automated Reasoning}",
	volume        = 3097,
	year          = 2004,
}

Contents (36 items)

6 ×#proving
5 ×#logic
4 ×#constraints
4 ×#formal method
4 ×#named
3 ×#finite
3 ×#order
3 ×#performance
3 ×#using
2 ×#algorithm

IJCAR-2004-MeseguerR #analysis #formal method #logic #semantics #specification #tool support

Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools (JM, GR), pp. 1–44.

IJCAR-2004-Lochner #order

A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting (BL), pp. 45–59.

IJCAR-2004-RiazanovV #constraints #performance

Efficient Checking of Term Ordering Constraints (AR, AV), pp. 60–74.

IJCAR-2004-ThiemannGS #composition #dependence #proving #termination #using

Improved Modular Termination Proofs Using Dependency Pairs (RT, JG, PSK), pp. 75–90.

IJCAR-2004-GodoyT #term rewriting

Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure (GG, AT), pp. 91–106.

IJCAR-2004-BofillR #order

Redundancy Notions for Paramodulation with Non-monotonic Orderings (MB, AR), pp. 107–121.

IJCAR-2004-KazakovN #transitive

A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards (YK, HdN), pp. 122–136.

IJCAR-2004-SteelBM #induction #protocol

Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures (GS, AB, MM), pp. 137–151.

IJCAR-2004-ZhangSM #constraints #data type #integer #recursion

Decision Procedures for Recursive Data Structures with Integer Constraints (TZ, HBS, ZM), pp. 152–167.

IJCAR-2004-GanzingerSW #composition #proving #similarity

Modular Proof Systems for Partial Functions with Weak Equality (HG, VSS, UW), pp. 168–182.

IJCAR-2004-BaaderGT #decidability #logic #problem #word

A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics (FB, SG, CT), pp. 183–197.

IJCAR-2004-DenneyFS #automation #proving #theorem proving #using

Using Automated Theorem Provers to Certify Auto-generated Aerospace Software (ED, BF, JS), pp. 198–212.

IJCAR-2004-MaricJ #framework #named #platform

argo-lib: A Generic Platform for Decision Procedures (FM, PJ), pp. 213–217.

IJCAR-2004-MouraORRS #deduction #embedded

The ICS Decision Procedures for Embedded Deduction (LMdM, SO, HR, JMR, NS), pp. 218–222.

IJCAR-2004-Schulz

System Description: E 0.81 (SS), pp. 223–228.

IJCAR-2004-Gottlob #finite #higher-order #logic #research

Second-Order Logic over Finite Structures — Report on a Research Programme (GG), pp. 229–243.

IJCAR-2004-GilHSZ #algorithm #constraints #finite #order #performance #problem

Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains: Extended Abstract (ÀJG, MH, GS, BZ), pp. 244–258.

IJCAR-2004-LutzW #source code

PDL with Negation of Atomic Programs (CL, DW), pp. 259–273.

IJCAR-2004-Larchey-Wendling #logic

Counter-Model Search in Gödel-Dummett Logics (DLW), pp. 274–288.

IJCAR-2004-LetzS

Generalised Handling of Variables in Disconnection Tableaux (RL, GS), pp. 289–306.

IJCAR-2004-Tammet #semantics #web

Chain Resolution for the Semantic Web (TT), pp. 307–320.

IJCAR-2004-TurhanK #named #standard

Sonic — Non-standard Inferences Go OilEd (AYT, CK), pp. 321–325.

IJCAR-2004-HustadtKRV #named #proving

TeMP: A Temporal Monodic Prover (UH, BK, AR, AV), pp. 326–330.

IJCAR-2004-WintersteinBG #diagrams #proving #theorem proving

Dr.Doodle: A Diagrammatic Theorem Prover (DW, AB, CAG), pp. 331–335.

IJCAR-2004-Weispfenning #constraints

Solving Constraints by Elimination Methods (VW), pp. 336–341.

IJCAR-2004-Subramani #integer #quantifier #source code

Analyzing Selected Quantified Integer Programs (KS), pp. 342–356.

IJCAR-2004-AvigadD #formal method #higher-order

Formalizing O Notation in Isabelle/HOL (JA, KD), pp. 357–371.

IJCAR-2004-MengP #interactive #proving #using

Experiments on Supporting Interactive Proof Using Resolution (JM, LCP), pp. 372–384.

IJCAR-2004-BartheCT #formal method #random

A Machine-Checked Formalization of the Generic Model and the Random Oracle Model (GB, JC, ST), pp. 385–399.

IJCAR-2004-ColtonMSM #algebra #automation #classification #finite #generative #theorem

Automatic Generation of Classification Theorems for Finite Algebras (SC, AM, VS, RLM), pp. 400–414.

IJCAR-2004-Avenhaus #algorithm #performance #permutation

Efficient Algorithms for Computing Modulo Permutation Theories (JA), pp. 415–429.

IJCAR-2004-TourE #equation

Overlapping Leaf Permutative Equations (TBdlT, ME), pp. 430–444.

IJCAR-2004-Bonichon #deduction #named

TaMeD: A Tableau Method for Deduction Modulo (RB), pp. 445–459.

IJCAR-2004-Beeson #logic

Lambda Logic (MB), pp. 460–474.

IJCAR-2004-Farmer #calculus #formal method

Formalizing Undefinedness Arising in Calculus (WMF), pp. 475–489.

IJCAR-2004-SutcliffeS #contest

The CADE ATP System Competition (GS, CBS), pp. 490–491.