[TYPES] IJCAR 2004 call for participation
Maria Paola Bonacina
mariapaola.bonacina at univr.it
Tue May 4 01:33:24 EDT 2004
-------------- next part --------------
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
to Formal Analysis Tools
Author: José Meseguer
Paper Title: A redundancy criterion based on ground reducibility by ordered rewriting
Author: Bernd Löchner
-------------------------------------------------------------------------------------
10.30 PAUSE
-------------------------------------------------------------------------------------
11.00 Saturation-based theorem-proving
Paper Title: Redundancy notions for paramodulation with non-monotonic orderings
Authors: Miquel Bofill and Albert Rubio
Paper Title: A Resolution decision procedure for the guarded fragment with transitive guards
Authors: Yevgeny Kazakov, and Hans de Nivelle
Paper Title: Attacking a protocol for group key agreement by refuting incorrect inductive conjectures
Authors: Graham Steel, Alan Bundy, and Monika Maidl
-------------------------------------------------------------------------------------
11.00 Higher-order reasoning
Paper Title: TAMED: A Tableau method for deduction modulo
Author: Richard Bonichon
Paper Title: Lambda logic
Author: Beeson Michael
Paper Title: Formalizing undefinedness arising in calculus
Author: William M. Farmer
-------------------------------------------------------------------------------------
12.30 LUNCH
-------------------------------------------------------------------------------------
14.00 Combination techniques
Paper Title: Decision procedures for recursive data structures with integer constraints
Authors: Ting Zhang, Henny Sipma, and Zohar Manna
Paper Title: Modular proof systems for partial functions with weak equality
Authors: Harald Ganzinger, Viorica Sofronie-Stokkermans, and Uwe Waldmann
Paper Title: A New combination procedure for the word problem that
generalizes fusion decidability results in modal logics
Authors: Franz Baader, Silvio Ghilardi, and Cesare Tinelli
-------------------------------------------------------------------------------------
15.30 PAUSE
-------------------------------------------------------------------------------------
16.00 Verification and systems
Paper Title: Using automated theorem provers to certify auto-generated aerospace software
Authors: Ewen Denney, Bernd Fischer, and Johann Schumann
Paper Title: ARGO-LIB: A Generic platform for decision procedures
Authors: Filip Maric and Predrag Janicic
Paper Title: The ICS decision procedures for embedded deduction
Authors: Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, and Natarajan Shankar
Paper Title: System description: E~0.81
Author: Stephan Schulz
-------------------------------------------------------------------------------------
18.00 END
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
JULY 7 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9.00 Reasoning with finite structures
Invited Talk : Second Order Logic over Finite Structures -- Report on a Research Programme
Author: Georg Gottlob
Paper Title: Efficient algorithms for constraint description problems over finite totally ordered domains
Authors: Angel J. Gil, Miki Hermann, Gernot Salzer, and Bruno Zanuttini
--------------------------------------------------------------------------------------
10.30 PAUSE
--------------------------------------------------------------------------------------
11.00 Tableaux and non-classical logics
Paper Title: PDL with negation of atomic programs
Authors: Carsten Lutz and Dirk Walther
Paper Title: Counter-model search in Gödel-Dummett logics
Author: Dominique Larchey-Wendling
Paper Title: Generalised handling of variables in disconnection tableaux
Authors: Reinhold Letz and Gernot Stenz
--------------------------------------------------------------------------------------
11.00 Rewriting II
Paper Title: Efficient checking of term ordering constraints
Authors: Alexandre Riazanov and Andrei Voronkov
Paper Title: Improved modular termination proofs using dependency pairs
Authors: Rene Thiemann, Juergen Giesl, and Peter Schneider-Kamp
Paper Title: Deciding fundamental properties of collapsing systems by rewrite closure
Authors: Guillem Godoy and Ashish Tiwari
--------------------------------------------------------------------------------------
12.30 LUNCH
--------------------------------------------------------------------------------------
EXCURSION
--------------------------------------------------------------------------------------
20.00 CONFERENCE DINNER
--------------------------------------------------------------------------------------
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
JULY 8 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9.00 Computer mathematics
Invited Talk : Solving Constraints by Elimination Methods
Author: Volker Weispfenning
Paper Title: Analyzing selected quantified integer programs
Author: K. Subramani
--------------------------------------------------------------------------------------
10.30 PAUSE
--------------------------------------------------------------------------------------
11.00 Interactive Theorem Proving
Paper Title: Formalizing O notation in Isabelle/Hol
Authors: Jeremy Avigad and Kevin Donnelly
Paper Title: Experiments on supporting interactive proof using resolution
Authors: Jia Meng and Lawrence C. Paulson
Paper Title: A Machine-checked formalization of the generic model and the random oracle model
Authors: Gilles Barthe, Jan Cederquist, and Sabrina Tarento
--------------------------------------------------------------------------------------
11.00 Combinatorial reasoning
Paper Title: Automatic generation of classification theorems for finite algebras
Authors: Simon Colton, Andreas Meier, Volker Sorge and Roy McCasland
Paper Title: Efficient algorithms for computing modulo permutation theories
Author: Jürgen Avenhaus
Paper Title: Overlapping leaf permutative equations
Authors: Thierry Boy de la Tour and Mnacho Echenim
--------------------------------------------------------------------------------------
12.30 LUNCH
--------------------------------------------------------------------------------------
14.00 Applications and systems
Paper Title: Chain resolution for the semantic web
Author: Tanel Tammet
Paper Title: SONIC - Non-standard inferences go oiled
Authors: Anni-Yasmin Turhan and Christian Kissig
Paper Title: TEMP: A Temporal monodic prover
Authors: Ullrich Hustadt, Boris Konev, Alexandre Riazanov and Andrei Voronkov
Paper Title: DR.DOODLE: A Diagrammatic theorem prover
Authors: Daniel Winterstein, Alan Bundy and Corin Gurr
--------------------------------------------------------------------------------------
16.00 END
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
More information about the Types-list
mailing list