[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