lescanne@LORIA.CRIN.FR (Pierre Lescanne) (03/07/91)
RTA-91: PRELIMINARY PROGRAM Fourth International Conference on Rewriting Techniques and Applications April 10-12, 1991 Como, Italy For information about registration, etc., see below or contact Professor G. Degli Antoni or Dr. Marelva Bianchi Dipartimento di Scienze dell'Informatione Universita degli Studi di Milano Via Moretto da Brescia, 9 I - 20133 Milano, Italy Telephone: +39.2.7575.201 / 209 +39.2.7575.257 FAX: +39.2.7611.0556 e-mail: gdantoni@imisiam.BITNET WEDNESDAY, 10 APRIL ___________________ ___________________ 8:30-8:45 Opening. SESSION 1 G. Smolka (U. Saarbrucken), Chair. 8:45-9:10 Transfinite reductions in orthogonal term rewriting systems. J. R. Kennaway (U. East Anglia), J. W. Klop (CWI, Amsterdam), M. R. Sleep (U. East Anglia), and F. J. de Vries (CWI, Amsterdam) 9:15-9:40 Redex captured in term graph rewriting. W. Farmer and R. Watro (MITRE Corp., Bedford) 9:45-10:10 Rewriting, narrowing, and equational unification: the higher-order cases. D. A. Wolfram (Oxford U.) 10:15-10:40 Adding algebraic rewriting to the untyped lambda calculus. D. Dougherty (Wesleyan U.) 10:40-11:10 BREAK SESSION 2 L. Bachmair (SUNY at Stony Brook), Chair. 11:10-11:35 Incremental termination proofs and the length of derivations. F. Drewes (U. Bremen) and C. Lautemann (U. Mainz) 11:40-12:05 Time bounded rewrite systers and termination proofs by generalized embedding. D. Hofbauer (TU Berlin) 12:10-12:35 Detecting redundant narrowing derivations by the LSE-SL test. A. Bockmayr and S. Krischer (U. Karlsruhe) 12:35-14:30 LUNCH SESSION 3 U. Martin (U. London and MIT), Chair. 14:30-14:55 Unification, weak unification, upper bound, lower bound, and generalization problems. F. Baader (U. Kaiserslautern) 15:00-15:25 AC unification through order-sorted AC1 unification. E. Domenjoud (CNRS and INRIA, Nancy) 15:30-15:55 Narrowing directed by a graph of terms. J. Chabin and P. Rety (U. Orlans) 16:00-16:25 How algebra can help in equational unification. F. Baader and W. Nutt (U. Kaiserslautern) 16:25-16:55 BREAK SESSION 4 C. Kirchner (INRIA, Nancy), Chair. 16:55-17:20 Undecidable properties of syntactic theories. F. Klay (INRIA, Nancy) 17:25-17:50 Goal directed strategies for paramodulation. W. Snyder and C. Lynch (Boston U.) 17:55-18:20 Minimal solutions of linear diophantine systems: bounds and algorithms. L. Pottier (INRIA, Sophia Antipolis) ________________________________________________________ THURSDAY, 11 APRIL SESSION 5 H. Ganzinger (U. Dortmund), Chair. 8:30-8:55 Proofs in parametrized specifications. H. Kirchner (CNRS and INRIA, Nancy) 9:00-9:25 Completeness of combinations of constructor systems. A. Middeldorp (CWI, Amsterdam) and Y. Toyama (CWI, Amsterdam and NTT Labs.) 9:30-9:55 Modular higher-order E-unification. T. Nipkow (U. Cambridge) and Z. Qian (U. Bremen) 10:00-10:25 On confluence for weakly normalizing systems. P-L Curien (CNRS, Paris) and G. Ghelli (U. Pisa) 10:25-10:55 BREAK SESSION 6 L. Bachmair (Stony Brook), Chair. 10:55-11:20 Program transformation and rewriting. F. Bellegarde (Oregon Grad. Inst.) 11:25-11:50 An efficient representation of arithmetic for term rewriting. D. Cohen (Royal Holloway and Bedford New College) and P. Watson (Glasgow U.) 11:55-12:20 Query optimization using conditional and unconditional rewrite rules. S. van Denneheuval, K. Kwast, E. Spaan (U. Amsterdam), and Renardel de Lavalette (U. Utrecht) 12:20-14:30 LUNCH SESSION 7: F. Otto (U. Kassel), Chair 14:30-14:55 Boolean algebra admits no canonical term rewriting system. R. Socher-Ambrosius (U. Kaiserslautern and SUNY, Stony Brook) 15:00-15:25 Decidability of confluence and termination of monadic term rewriting systems. K. Salomaa (U. Turku) 15:30-15:55 Bottom-up tree pushdown automata and rewrite systems. J-L Coquide, M. Dauchet, R. Gilleron ( U. Lille ), and S. Vagvolgyi (Hungerian Acad. Sci., Szeged) 16:00-16:25 On relationship between term rewriting systems and regular tree languages. G. Kucherov (USSR Acad. Sci., Novosibirsk) 16:25-16:55 BREAK SESSION 8 R. Book (UC Santa Barbara), Chair. 17:00-17:25 The equivalence of boundary and confluent graph grammars on graph languages with bounded degree. F. Brandenburg, U. Passau 17:30-17:55 Left-to-right tree pattern matching. A. Graef (U. Mainz) 18:00-18:25 Incremental techniques for efficient normalization of nonlinear rewrite systems. R. Ramesh (U. Texas - Dallas) and I.V. Ramakrishnan (SUNY at Stony Brook) _______________________________________________________ FRIDAY. 12 APRIL SESSION 9 F. Winkler (U. Linz), Chair. 8:45-9:10 On fairness of completion-based theorem proving strategies. M. P. Bonacina (U. Milano and SUNY at Stony Brook) and J. Hsiang (SUNY at Stony Brook) 9:15-9:40 Proving inductive theorems by completion and embedding techniques. J. Avenhaus (U. Kaiserslautern) 9:45-10:10 Divergence phenomena during completion. A. Sattler-Klein (U. Kaiserslautern) 10:15-10:40 Simulating Buchberger's algorithm by Knuth-Bendix completion. R. Buendgen (U. Tuebingen) 10:40-11:10 BREAK SESSION 10 C. Kirchner (INRIA, Nancy), Chair. 11:10-11:35 On proving properties of completion strategies. M. Hermann (CNRS and INRIA, Nancy) 11:40-12:05 On AC-termination and ground AC-completion. C. Marche (U. Paris-Sud) 12:10-12:35 Any ground associative-commutative theory has a finite canonical system. P. Narendran (SUNY at Albany) and M. Rusinowitch (CNRS and INRIA, Nancy) FINI ________________________________________________________ SYSTEMS DEMONSTRATIONS A narrowing-based theorem prover. U. Fraus (U. Passau) and H. Hussmann (TU Muenchen) ANIGRAF: An interactive systerm for the animation of graph rewriting systems with priorities. M. Billaud (U. Bordeaux) EMMY: A refutational theorem prover for first-order logic with equations. A. Deruyer (U. Lille and SUNY at Stony Brook) The Tecton Proof System. R. Agarwal (Rensselaer Poly. Inst.), D. Kapur (SUNY at Albany), D. Musser (Rensselaer Poly. Inst.), X. Nie (SUNY at Albany) ============================================================================== RTA '91 - Conference registration form Please send this registration form with payment to: Centro di Cultura Scientifica "A. Volta" - Villa Olmo, Via Cantoni 1 - 22100 Como (Italy). Advanced registration discount are available to all registration forms received, with full payment, post-marked on or before 28/02/1991. Please bring your registration acknowledgment with you. Notices on cancellation must be received in writing at Centro "A. Volta" before 15/03/1991. Registration fees will include proceedings, lunches, dinners, additional informative material, on site reception hostesses. First name _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Surname _ _ _ _ _ _ _ _ _ _ _ Position _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Institution _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Address _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ City _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ State _ _ _ _ _ _ _ _ _ _ _ Zip _ _ _ _ _ Phone _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Telex _ _ _ _ _ _ _ _ Fax _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ E-mail _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Please specify society name and name of Association (EATCS, IEEE, ACM, SIGART, ...) : Society name _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Association _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Proceedings A preprint copy of the Conference proceedings - edited by Springer Verlag - will be distributed to the attendees. Supplementary copies can be bought on site. Payment Please send the amount corresponding to the full amount of the registration by: International Postal Money Order or Eurocheque. Payment should be addressed to Centro di Cultura Scientifica "A. Volta" - Villa Olmo, Via Cantoni 1 - 22100 Como (Italy) and be effected in italian liras net of all bank charges (if not possible, U.S. dollars will be accepted). Further possibility is payment by Banker's draft drawn on Banco Lariano - P.zza Cavour 15 - 22100 Como (Italy) - c/c 479619/3 headed to "Centro di Cultura Scientifica Alessandro Volta"; in this case, please consider high bank charges. A check or money order must accompany your registration form. REGISTRATION FEES RTA '91 Advanced registration On site registration Attendees Lit. 300.000 Lit. 350.000 Lecturers Lit. 230.000 Lit. 280.000 Commitee members Lit. 200.000 Lit. 230.000