東北大学・電気通信研究所・外山研究室ではNUEセミナーを開催しています． テーマはプログラム理論や定理自動証明を中心に， 情報科学の理論的なさまざまな話題をとりあげています． 興味をおもちの方はどなたでもフラリと気楽におたちより下さい．
| 日時 | 2002年12月5日 |
|---|---|
| 講演者 | 青戸 等人 (群馬大) |
| 題目 | 単純型付き項書換え系の停止性について |
| 要旨 | 単純型付き項書換え系は，山田 (RTA'01, 2001) によって提案された， 高階関数を利用できる項書換え系である．通常の高階項書換え系と異なり，こ の項書換え系は束縛変数を組み込んでいない．単純型付き項書換え系の停止性 証明法について紹介する． |
| 日時 | 2002年3月20日 |
|---|---|
| 講演者 | 有村 博紀（九州大学大学院システム情報科学研究院) |
| 題目 | ウェブと半構造データからのデータマイニング |
| 要旨 | データマイニング (Data Mining) は，データベースに蓄積された大量 のデータから，自明でない規則性をとりだす方法についての研究であり，1990 年代初頭から，ビジネス分野や自然科学分野で活発に研究されている．本講演 では，われわれのグループで研究を進めているテキストデータと半構造データ を対象としたデータマイニングについて紹介する． |
| 日時 | 2002年3月8日 |
|---|---|
| 講演者 | Herman Geuvers (Nijmegen University) |
| 題目 | Open terms and Open proofs: a plea for Interactive Logic |
| 要旨 |
In computer assisted theorem proving, unfinished proofs
occur as the output of tactics: Suppose that starting from goal A, if
we apply tactic T, the system returns goal B. This means that the
system has created a `proof-with-a-hole' of A and this hole consists
of a (yet to be produced) proof of B. Unfinished terms occur only in
some type theory based theorem provers (like Coq or Lego). For
example, when proving (exists x ( A(x) )), one may continue proving
A(?), leaving the specific choice for (?) (temporarily) open. Note
that here the `open term' (?) occurs in the expression of a goal and
hence in an `open proof'. Allowing open terms in (open) proofs occurs
quite naturally when we prove a theorem and it gives a greater
flexibility to the proving process. At the same time, open terms
obscure the formal status and meaning of the `unfinished proof' (in
terms of the underlying logic), because logic itself does not deal
with unfinished proofs. (The derivation rules give an inductive
definition of what the derivable judgments are.) In this talk we want to give a detailed account of open terms and open proofs, thus giving a formal explanation of `interactive higher order logic'. Then we define the type theoretic variant of this, in which open proofs and open terms become first class citizens. In this system we can formally define the notion of `proof statte' and `tactic'. Joint work with Georgi Jojgov (Eindhoven, NL). This work builds on previous work by Conor McBride (Durham UK), see http://www.dur.ac.uk/c.t.mcbride/oleg/quiet/ |
| 日時 | 2002年3月5日 |
|---|---|
| 講演者 | Herman Geuvers (Nijmegen University) |
| 題目 | Preservation of SN for explicit substitution by using the RPO method |
| 要旨 |
We consider a refinement of beta-reduction on lambda
calculus where substitution is made explicit (not global). This
refinement can be (and has been in the literature) defined in various
ways, obtaining bx-reduction, where the b-step creates the explicit
substitution and the x-steps move the substitutions through the term
and execute them. Some refinements lead to the situation that some
term M is beta-SN, but not bx-SN, which is clearly an undesirable
situation: we want the explicit substitution calculus to "preserve
strong normalization". If the calculus bx preserves strong
normalization, we say that it has the PSN property. We present our own calculus bx and we prove that it satisfies the PSN property. Our proof uses the RPO (recursive path ordering) method. Then we show that our proof method is very general and can be used for other explicit substitution calculi as well. We also illustrate on some extensions of bx where the PSN property brakes down. Joint work with Roel Bloo (Eindhoven, NL), Reference: R. Bloo and H. Geuvers, Explicit Substitution. On the Edge of Strong Normalization, Theoretical Computer Science 211 (1999), pp 375 -- 395. |
まで．