第 214 回 PTT のお知らせ
日時: 1995年12月21日 (木) 18:30 から
場所: 富士ゼロックス株式会社
KSPソフトウェア事業所 4F A473会議室
JR南武線武蔵溝の口駅,東急田園都市線溝の口駅下車.
田園都市線利用者は南武線乗り換え口を出て,まっすぐ
南武線に沿って進む.南武線利用者は,改札を出て
すぐ右に曲がり南武線に沿って進む.
どちらも約1000m進むと左手にNEC東京第二工場があるので,
その右端の塀に沿い約50m進むと,かながわサイエンス
パーク(KSP) (淡い紫色のビル)の前に着く.X字した棟の
手前側のエレベータに乗り,4階で降りる.エレベータ
ホールから左手に進むと会議室があります.
KSPへのシャトルバス(無料)もあります. 乗り場まで駅から
徒歩で5分ほど, シャトルバスに乗って3分ほどで着きます.
バス停は, JR溝の口駅改札から右手へ南武線沿いに100mほど進み,
横断舗道を渡って, 進行方向左手に工事現場を見ながら,
そのまま100mほど直進した右側にあります.
話者: 坂井公 (筑波大学数学系)
題目: 直観主義命題論理の定理証明器作成の試み
概要:
直観主義命題論理の定理証明器をプログラミング言語 Prolog を使っ
て作成した。システムは、与えられた命題論理式に対して、それが恒
真ならばLJ による証明図を、恒真でなければ Kripke モデルによる
反例を求めるものである。証明図の表示にあたっては、あまり手間を
掛けずにできる範囲でできるだけ簡潔な証明図を得ることに工夫を凝
らした。また、その時の考察から、LJ を変形した多少弱い形の形式
的推論体系でも完全になることがわかったので、それについても簡単
に述べる。
食事:
当日発表終了後、忘年会を行います。
会費は5,000円程度を予定しています。会場の予約の都合上、
忘年会にご参加される予定の方は、お手数ですが、
伊知地(富士ゼロックス システム・コミュニケーション研究所)
e-mail hiro@crl.fujixerox.co.jp
FAX 0465-81-8983
あて、20日(水)までにご連絡下さい。
次々回:
1996年1月 ?? 日 (木) 東工大
葉書の残りは ?? 枚です
差出人(幹事):
〒184 東京都小金井市中町2-24-16
東京農工大学 工学部 電子情報工学科
コンピュータサイエンスコース
並木美太郎
Tel. 0423-88-7139 ダイヤルイン
namiki@cc.tuat.ac.jp
iijima@ae.keio.ac.jp