トップ «前の日記(2003-09-25) 最新 次の日記(2003-09-27)» 月表示 編集

日々の流転


2003-09-26 [長年日記]

λ. 西岡研

暇だったので覗いてみることに。符号理論がテーマで代数の入門から。

シラバスには

とっつきにくい代数系ではあるが、近年の計算機の発達のおかげで、大変な計算も記号的に処理され、瞬時に結果が得られるようになってきた。このため、学習する手法もすこし変わってきつつある。

と書いてあったので、Computer Algebra Systems をバリバリ使って学習/研究することを期待してみる。

λ. "Topology via Logic" を輪講することに

今期は"Topology via Logic"を輪講することになった、……というかした。やるぞー

λ. Otter: An Automated Deduction System

Our current automated deduction system Otter is designed to prove theorems stated in first-order logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. Otter can also be used as a symbolic calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne National Laboratory deduction system whose ancestors (dating from the early 1960s) include the TP series, NIUTP, AURA, and ITP.

Currently, the main application of Otter is research in abstract algebra and formal logic. Otter and its predecessors have been used to answer many open questions in the areas of finite semigroups, ternary Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry.

メモ。paramodulationって何?

【2006-06-29追記】 萩谷先生の「命題論理の演繹体系」という講義録にparamodulationの解説がある。

λ. ACL

についてちょっと調べてみる。

λ. 夕食

水龍。

λ. 誕生日

というわけで今日は誕生日でした。本当に色々な人に祝ってもらえて、とても嬉しかったです。どうもありがとうございます。

川井君にアイスクリームをおごってもらった。

それから、Zinniaさんにねういちさんという方と同じ誕生日だと教えてもらいました。これまで不思議と同じ誕生日の人に会ったことがなかったので、ちょっと嬉しい。それに、この方のTODOには「rubyの勉強」「卒研」「親知らずを抜く」といったキーワードが並んでいて、何だか親近感を感じるのでした (^^;

本日のツッコミ(全2件) [ツッコミを入れる]
ψ ねういち (2003-09-28 17:37)

始めまして。<br>生まれも1981年でまったく同じ日に生まれたんですね〜。<br>何か縁があるのかも!(笑)

ψ さかい (2003-09-29 21:36)

どうも始めまして。<br>ねいうちさんも誕生日おめでとうございます。<br>何か縁があるといいですね(笑)