[logic-ml] 直前のお知らせ：Jouannaud氏Talk; Sept 22nd (木曜夕方)Mita Logic Seminar, on completion methods

[Mitsu Okada]

****MITA LOGIC SEMINAR; PROF. J- P JOUANNAUD'S TALK and a discussion 
session****
******************************************************************************* 

(The meeting is open to everyone without any preregistration)

Theme "Completion methods, in Logic, algebra and Computer science"

The Knuth-style completion procedure bridges Logic, Algebra and 
Computation. The aim of this meeting is to discuss the completion issue
from the logical, algebraic, computer-scientific, historical and 
philosophical points of view.


Date/Time Sept 22 Thursday 16:30pm-18:00pm
Place: Meeting Room number 1, Basement of North Building (Hita-Kan),
Mita Campus of Keio University; 5 minutes walking distance from 
JR-Tamachi, Subway-Mita or Subway-Akabanebashi.
we recommend to you to use the East Gate where you find a security guard 
to ask the exact direction to the Meeting Room,
if it is not clear for you with the campus map on our university's homepage.

Main Speaker: Prof. Jean-Pierre Jouannaud, Professor of l'Ecole 
polytechnique and of INRIA, (French National Instutute of Computer Science)
as well as the Ｓｏｆｔｗａｒｅ Chair of :INRIA- Tsinghua(精華大学) Beijing.

Title:
A complete tour of completion methods

After the talk, we plan to have a discussion session on Knuth-Huet 
completions and some ther completion issues from the historical, 
mathematical, computer-scientific and philosophical view points.Af

Abstract
We shall present a unified view of completion methods in abstract 
algebras (Knuth and Bendix ; Peterson and Stickel; Huet; Jouannaud and 
Kirchner; Bachmair Dershowitz and Hsiang; Marché; Jouannaud Liu and Luo) 
and polynomial rings (Janet, Hironaka, Buchberger, Mora). Indeed, there 
are two quite different completion methods: Janet's methods, based on 
maintaining an inter-reduced system as a completion invariant, and all 
the others, based on reaching an inter-reduced system in the limit. As a 
result, we derive a new completion algorithm for abstract algebras. We 
conclude with a set of open problems when using an ill-founded 
completion order (inspired from Hironaka's local ring computation 
technique).


Profile of the guest speaker:
Jean-Pierre Jouannaud graduated from Ecole Polytechnique de Paris and 
obtained his doctorate from University Paris 6 in 1978. He was then a 
professor at the universities of Nancy, Paris-Sud, and at Ecole 
Polytechnique successively, as well as an invited professor at a number 
of places, including Stanford Research Institute and Stanford University 
in US, the University of Barcelona in Spain, Keio University in Japan 
and National Taiwan University in Taiwan. He is now a visiting chair 
professor at Tsinghua University in Beijing, China, holding a joint 
appointment with INRIA, the French research institute in ICT.

His current research interests are at the interplay between deduction 
rules, rewrite rules, decision procedures and type theory, in the 
development of proof assistants (in particular, Coq, a leading open 
source proof assistant), and in their application to the formal proof of 
systems. He is the head of FORmal Methods for Embedded Systems, a joint 
project of LIAMA, the french-chinese consortium hosting their 
collaborative research in ICT of which he is the current french 
director. He published over 100 papers, among which 10 have over one 
hundred citations each. He won several awards during his career, 
including the "Prix Montpetit" of the french "Academie des Sciences" and 
the price for international scientific collaboration delivered by the 
"Academie des Sciences" and the National Research Council of Taiwan.

He was on the program committee of a number of major international 
conferences including LICS (chair in 2011), ICALP, CSL, MFCS, FPLCA, 
RTA, CADE, etc. He created the International Conference on Rewriting 
Techniques and Applications, the International Conference on Constraints 
in Computational Logics which later merged with
"Constraints" , the international workshops UNIF and CTRS, and the 
international conference on Certified Proofs and Programs to be held for 
the first time in 2011 in Kenting, Taiwan. He has been or is a member of 
the editorial boards of the Journal of Symbolic Computation, Information 
and Computation, Constraints, Progress in Theoretical Computer Science, 
and the International Journal of Softare and Informatics. He has been a 
member of the scientific council of the European Association for 
Computer Science Logic and of the European Association for Theoretical 
Computer Science. He has also been a member of the "Fachbeirat" of the 
Max Planck Institute for Computer Science, and is now on the scientific 
visiting committee of Academia Sinica, Taiwan. He chaired the jury of 
the Goedel prize awarded jointly by the EATCS and ACM-SIGACT in 2010, 
was a member of the jury of the Goedel prize (2008, 2009, 2010), of the 
LICS "test of time award" 2010, of the Kleene Price 2010, and of the 
Ackerman price 2011


ご不明な点がございましたら、logic at abelard.flet.keio.ac.jp (論理とオント 
ロジーオープンリサーチセンター事務局まで、ご連絡ください。　岡田光弘、慶応大

-------------------------------
.