[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[no subject]
=09by mizar.uwb.edu.pl (Postfix) with ESMTP id DAA7E2089D
=09for <mizar-forum@mizar.uwb.edu.pl>; Tue, 4 May 2004 00:20:32 +0200 (CES=
T)
Received: from mailgw.univr.it (mailgw.univr.it [157.27.6.150])
=09by mailgate.uwb.edu.pl (8.11.6p2-18092003/8.11.6) with SMTP id i43MMEW31=
137
=09for <mizar-forum@mizar.uwb.edu.pl>; Tue, 4 May 2004 00:22:14 +0200
Received: (qmail 30768 invoked from network); 3 May 2004 22:01:01 -0000
Received: from unknown (HELO profs.sci.univr.it) (157.27.252.10)
by mailgw.univr.it with SMTP; 3 May 2004 22:01:01 -0000
Received: from sci.univr.it (guest@profs [157.27.252.10])
=09by profs.sci.univr.it (8.9.3/8.9.3) with SMTP id AAA05098
=09for <mizar-forum@mizar.uwb.edu.pl>; Tue, 4 May 2004 00:19:18 +0200 (MET =
DST)
Received: from 82.48.242.157
(SquirrelMail authenticated user bonacina)
by profs.sci.univr.it with HTTP;
Tue, 4 May 2004 00:20:18 +0200 (MET DST)
Message-ID: <49336.82.48.242.157.1083622818.squirrel@profs.sci.univr.it>
Date: Tue, 4 May 2004 00:20:18 +0200 (MET DST)
Subject: [mizar] IJCAR 2004 call for participation
From: "Maria Paola Bonacina" <mariapaola.bonacina@univr.it>
To: <mizar-forum@mizar.uwb.edu.pl>
X-Priority: 3
Importance: Normal
X-MSMail-Priority: Normal
X-Mailer: SquirrelMail (version 1.2.6)
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary=3D"----=3D_20040504002018_54972"
X-RAVMilter-Version: 8.4.2(snapshot 20021217) (mailgate)
Sender: owner-mizar-forum@mizar.uwb.edu.pl
Precedence: bulk
Reply-To: mizar-forum@mizar.uwb.edu.pl
------=3D_20040504002018_54972
Content-Type: text/plain; charset=3Diso-8859-1
Content-Transfer-Encoding: 8bit
------=3D_20040504002018_54972
Content-Type: text/plain; name=3D"CfparticipIJCAR2004.txt"
Content-Disposition: attachment; filename=3D"CfparticipIJCAR2004.txt"
IJCAR 2004
Call for participation
The Second International Joint Conference on Automated Reasoning (IJCAR)
is the fusion of several major conferences in Automated Reasoning:
* CADE (The International Conference on Automated Deduction),
* FTP (The International Workshop on First-Order Theorem Proving),
* TABLEAUX (The International Conference on Automated Reasoning with
Analytic Tableaux and Related Methods),
* CALCULEMUS (Symposium on the Integration of Symbolic Computation and
Mechanized Reasoning), and
* FroCoS (Workshop on Frontiers of Combining Systems).
These five events will join for the first time at the IJCAR conference
in Cork in July 2004.
Registration to IJCAR 2004 is open: the deadline for early registration is
May 21, 2004
Please see http://4c.ucc.ie/ijcar/ for all registration, accomodation,
and travel details.
Technical programme of the main conference
(please see http://4c.ucc.ie/ijcar/ for the full programme)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%=
%%%%%%%%%%
JULY 6
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%=
%%%%%%%%%%
9.00 Rewriting I
Invited Talk : Rewriting Logic Semantics: From Language Specifications=20
to Formal Analysis Tools
Author: Jos=E9 Meseguer=20
Paper Title: A redundancy criterion based on ground reducibility by ordered=
rewriting
Author: =09Bernd L=F6chner
---------------------------------------------------------------------------=
----------
10.30 PAUSE=20
---------------------------------------------------------------------------=
----------
11.00 Saturation-based theorem-proving=20
Paper Title: =09Redundancy notions for paramodulation with non-monotonic o=
rderings
Authors: =09Miquel Bofill and Albert Rubio
Paper Title: =09A Resolution decision procedure for the guarded fragment w=
ith transitive guards
Authors: =09Yevgeny Kazakov, and Hans de Nivelle=20
Paper Title: =09Attacking a protocol for group key agreement by refuting i=
ncorrect inductive conjectures
Authors: =09Graham Steel, Alan Bundy, and Monika Maidl
---------------------------------------------------------------------------=
----------
11.00 Higher-order reasoning=20
Paper Title: =09TAMED: A Tableau method for deduction modulo
Author: =09Richard Bonichon
Paper Title: =09Lambda logic
Author: =09Beeson Michael
Paper Title: =09Formalizing undefinedness arising in calculus
Author: =09William M. Farmer
---------------------------------------------------------------------------=
----------
12.30 LUNCH
---------------------------------------------------------------------------=
----------
14.00 Combination techniques=20
Paper Title: =09Decision procedures for recursive data structures with int=
eger constraints
Authors: =09Ting Zhang, Henny Sipma, and Zohar Manna
Paper Title: =09Modular proof systems for partial functions with weak equa=
lity
Authors: =09Harald Ganzinger, Viorica Sofronie-Stokkermans, and Uwe Waldman=
n=20
Paper Title: =09A New combination procedure for the word problem that=20
generalizes fusion decidability results in modal logics
Authors: =09Franz Baader, Silvio Ghilardi, and Cesare Tinelli
---------------------------------------------------------------------------=
----------
15.30 PAUSE=20
---------------------------------------------------------------------------=
----------
16.00 Verification and systems=20
Paper Title: =09Using automated theorem provers to certify auto-generated =
aerospace software
Authors: =09Ewen Denney, Bernd Fischer, and Johann Schumann
Paper Title: =09ARGO-LIB: A Generic platform for decision procedures
Authors: =09Filip Maric and Predrag Janicic
Paper Title: =09The ICS decision procedures for embedded deduction
Authors: =09Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, and Nat=
arajan Shankar
Paper Title: =09System description: E~0.81
Author: =09Stephan Schulz=20
---------------------------------------------------------------------------=
----------
18.00 END=20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%=
%%%%%%%%%%
JULY 7 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%=
%%%%%%%%%%%%%%%%%
9.00 Reasoning with finite structures=20
Invited Talk : Second Order Logic over Finite Structures -- Report on a Res=
earch Programme
Author: =09Georg Gottlob
Paper Title: =09Efficient algorithms for constraint description problems o=
ver finite totally ordered domains
Authors: =09Angel J. Gil, Miki Hermann, Gernot Salzer, and Bruno Zanuttini
---------------------------------------------------------------------------=
-----------
10.30 PAUSE=20
---------------------------------------------------------------------------=
-----------
11.00 Tableaux and non-classical logics
Paper Title: =09PDL with negation of atomic programs
Authors: =09Carsten Lutz and Dirk Walther=20
Paper Title: =09Counter-model search in G=F6del-Dummett logics
Author: =09Dominique Larchey-Wendling
Paper Title: =09Generalised handling of variables in disconnection tableau=
x
Authors: =09Reinhold Letz and Gernot Stenz
---------------------------------------------------------------------------=
-----------
11.00 Rewriting II=20
Paper Title: =09Efficient checking of term ordering constraints
Authors: =09Alexandre Riazanov and Andrei Voronkov
Paper Title: =09Improved modular termination proofs using dependency pairs
Authors: =09Rene Thiemann, Juergen Giesl, and Peter Schneider-Kamp
Paper Title: =09Deciding fundamental properties of collapsing systems by r=
ewrite closure
Authors: =09Guillem Godoy and Ashish Tiwari=20
---------------------------------------------------------------------------=
-----------
12.30 LUNCH
---------------------------------------------------------------------------=
-----------
EXCURSION=20
---------------------------------------------------------------------------=
-----------
20.00 CONFERENCE DINNER
---------------------------------------------------------------------------=
-----------
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%=
%%%%%%%%%%%
JULY 8 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%=
%%%%%%%%%%%%%%%%%%
9.00 Computer mathematics=20
Invited Talk : Solving Constraints by Elimination Methods
Author: Volker Weispfenning=20
Paper Title: =09Analyzing selected quantified integer programs
Author: =09K. Subramani=20
---------------------------------------------------------------------------=
-----------
10.30 PAUSE=20
---------------------------------------------------------------------------=
-----------
11.00 Interactive Theorem Proving=20
Paper Title: =09Formalizing O notation in Isabelle/Hol
Authors: =09Jeremy Avigad and Kevin Donnelly
Paper Title: =09Experiments on supporting interactive proof using resoluti=
on
Authors: =09Jia Meng and Lawrence C. Paulson
Paper Title: =09A Machine-checked formalization of the generic model and t=
he random oracle model
Authors: =09Gilles Barthe, Jan Cederquist, and Sabrina Tarento=20
---------------------------------------------------------------------------=
-----------
11.00 Combinatorial reasoning=20
Paper Title: =09Automatic generation of classification theorems for finite=
algebras
Authors: =09Simon Colton, Andreas Meier, Volker Sorge and Roy McCasland
Paper Title: =09Efficient algorithms for computing modulo permutation theo=
ries
Author: =09J=FCrgen Avenhaus=20
Paper Title: =09Overlapping leaf permutative equations
Authors: =09Thierry Boy de la Tour and Mnacho Echenim
---------------------------------------------------------------------------=
-----------
12.30 LUNCH
---------------------------------------------------------------------------=
-----------
14.00 Applications and systems=20
Paper Title: =09Chain resolution for the semantic web
Author: =09Tanel Tammet=20
Paper Title: =09SONIC - Non-standard inferences go oiled
Authors: =09Anni-Yasmin Turhan and Christian Kissig
Paper Title: =09TEMP: A Temporal monodic prover
Authors: =09Ullrich Hustadt, Boris Konev, Alexandre Riazanov and Andrei Vor=
onkov
Paper Title: =09DR.DOODLE: A Diagrammatic theorem prover
Authors: =09Daniel Winterstein, Alan Bundy and Corin Gurr=20
---------------------------------------------------------------------------=
-----------
16.00 END
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%=
%%%%%%%%%%%
------=3D_20040504002018_54972--