From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id QAA08668; Mon, 3 May 2004 16:09:23 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id QAA11151 for ; Mon, 3 May 2004 16:09:22 +0200 (MET DST) Received: from mailgw.univr.it (mailgw.univr.it [157.27.6.150]) by concorde.inria.fr (8.12.10/8.12.10) with SMTP id i43E9LSH019578 for ; Mon, 3 May 2004 16:09:21 +0200 Received: (qmail 55348 invoked from network); 3 May 2004 13:49:57 -0000 Received: from unknown (HELO profs.sci.univr.it) (157.27.252.10) by mailgw.univr.it with SMTP; 3 May 2004 13:49:57 -0000 Received: from univr.it (noctua.sci.univr.it [157.27.252.66]) by profs.sci.univr.it (8.9.3/8.9.3) with ESMTP id QAA13103 for ; Mon, 3 May 2004 16:07:00 +0200 (MET DST) Message-ID: <40965204.5080501@univr.it> Date: Mon, 03 May 2004 16:07:00 +0200 From: Maria Paola Bonacina Organization: Universita` degli Studi di Verona User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.4.2) Gecko/20040220 X-Accept-Language: it, en-us, en, fr-fr MIME-Version: 1.0 To: caml-list@pauillac.inria.fr Subject: [Caml-list] IJCAR 2004 call for participation X-Enigmail-Version: 0.76.5.0 X-Enigmail-Supports: pgp-inline, pgp-mime Content-Type: multipart/mixed; boundary="------------060500050602020203020806" X-Miltered: at concorde with ID 40965291.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; bonacina:01 bonacina:01 ijcar:01 2004:99 ijcar:01 2004:99 first-order:01 cork:99 2004.:99 ucc:99 ucc:99 bernd:01 orderings:01 miquel:01 fragment:01 X-Attachments: name="CfparticipIJCAR2004.txt" name="CfparticipIJCAR2004.txt" Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk This is a multi-part message in MIME format. --------------060500050602020203020806 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit --------------060500050602020203020806 Content-Type: text/plain; name="CfparticipIJCAR2004.txt" Content-Transfer-Encoding: 8bit Content-Disposition: inline; filename="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 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% --------------060500050602020203020806-- ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners