坂井 公 SAKAI Ko

Articles:  1-20 of 20

  • パズルの挑戦! 講評  [in Japanese]

    山崎 秀記 , 坂井 公

    日経サイエンス 35(5), 92-95, 2005-05

  • 「パズルの挑戦!」解答と講評  [in Japanese]

    田中 裕一 , 山崎 秀記 , 坂井 公

    日経サイエンス 34(8), 112-115, 2004-08

  • On Solving Algebraic Equations over a Field of Characteristic 2.  [in Japanese]

    FUJITA Hiroyuki , TAKAHASHI Kouichi , SAKAI Ko , Hiroyuki Fujita , Kouichi Takahashi , Ko^^- Sakai , 筑波大学博士課程数学研究科 , 電子総合研究所 , 筑波大学数学系 , Doctoral Program in Mathematics University of Tsukuba. , Electrotechnical Laboratory. , Institute of Mathematics University of Tsukuba.

    Conwayが考案した標数2の体On_2の上の代数方程式の解放について考察する.特にω^ω未満の順序数を係数として持つ4次以下の方程式の完全な解法を与える.

    コンピュータソフトウェア 00018(00003), 29-33, 2001-05-15

    References (9)

  • 体On₂上の代数方程式の求解について(その3)  [in Japanese]

    藤田 博征 , 高橋 孝一 , 坂井 公

    日本ソフトウェア科学会大会論文集 17, 1-4, 2000-09

  • 「結合子による高階単一化」再考  [in Japanese]

    FUJITA Hiroyuki , IKEDA Hiroshi , SAKAI Ko , Hiroyuki Fujita , Hiroshi Ikeda , Ko Sakai , 筑波大学理工学研究科 , 筑波大学数学研究科 , 筑波大学数学系 , Master's Program in Science and Engineering University of Tsukuba , Doctoral Program in Mathematics University of Tsukuba , Institute of Mathematics University of Tsukuba

    高階単一化のアルゴリズムとしては,Huetによる射影と模倣に基づく手法が有名である.これに対してDougherty提案の結合子を利用したアルゴリズムでは,高階単一化をナローイングで扱うことができ,射影や模倣による手法に比べ,著しく扱いが簡単になる.しかし,Doughertyの論文は理論的明解さに欠けるので,我々は,アルゴリズムやその健全性・完全性の証明の記述の簡素化を試みた.さらに修正したアルゴリ …

    コンピュータソフトウェア 00014(00002), 180-184, 1997-03-17

    References (8)

  • Metis - AS : A Software Development Support System with Algebraic Specification Techniques  [in Japanese]

    OHSUGA Akihiko , SAKAI Ko , HONIDEN Shinichi

    Metis-ASは代数的な仕様記述言語を用いたソフトウェア開発の支援を目的として、項書換え技術の研究環境Metis-ASに多ソート代数やモジュール化の概念を導入して実現されたシステムである。このシステムの特徴は、(1)柔軟なユーザ・インタフェースによって仕様の記述や検証を効率的にすすめる、(2)いくつかの形式的意昧論によって広範囲の記述段階を支援する、(3)項書換え技術に基づく強カな仕様解析・検証 …

    IPSJ Journal 36(5), 1192-1202, 1995-05-15

    IPSJ  IR  References (17)

  • A Verification Procedure for Algebraic Specifications by Metis - AS  [in Japanese]

    OHSUGA Akihiko , SAKAI Ko , HONIDEN Shinichi

    本稿では、代数的仕様を自動検証する手続きの実現について述べる。この手続きは、仕様によって定まる始代数上の定理を項書換え技術によって証明するもので、理諭的には等式論理の帰納的定理証明手続きを多ソート代数の場合へ拡張したものとなっている。ここでは、手続きの効率化手法に焦点をあてるとともに、手続きが無限実行される問題の救済についても考察する。

    IPSJ Journal 34(11), 2242-2250, 1993-11-15

    IPSJ  IR  References (21) Cited by (1)

  • A Procedure to Prove Inductive Theorems in Equational Theories  [in Japanese]

    OHSUGA Akihiko , SAKAI Ko , HONIDEN Shinichi

    等式論理の始モデルにおいて成立する式を等式論理の帰納的定理と呼ぶ.本論文では,帰納的定理を証明するための推論規則を与える.この推論規則に基づく証明手続きは,潜在帰納法と呼ばれる証明方法の拡張とみることができるが,向きづけのできない公理や定理を一般的に扱うことができ,更には,公理系に対応する完備な項書換え系が有限の要素で表現できない場合でも手続きを適用できる点が,従来の方法と異なる.推論規則は,反ば …

    The Transactions of the Institute of Electronics,Information and Communication Engineers. 76(3), 130-138, 1993-03-25

    References (16) Cited by (3)

  • 特集「制約論理プログラミング」の編集にあたって  [in Japanese]

    坂井 公

    コンピュータソフトウェア 9(6), 2, 1992-11-01

  • Inference Rules for a Complete Set of E-unfiries.  [in Japanese]

    大須賀 昭彦 , 坂井 公 , Akihiko Ohsuga , Ko Sakai , 東芝システム・ソフトウェア技術研究所 , 新世代コンピュータ技術開発機構

    等式理論を法として単一化を行う拡張単一化のことをE単一化という.本稿では,E単一化を行う半決定手続きを与える.この手続きは,任意の等式理論に対して完全である.完全性の証明には証明順序法を用いる.また手続きは,Knuth-Bendix完備化手続きの拡張になっているので,E単一化の過程で等式理論に対応する完備な項書換え系を獲得することもある.この場合,本稿はHullotの結果の一般化でもある.

    コンピュ-タソフトウェア 8(3), p241-262, 1991-05

  • CAP: Computer Aided Proof  [in Japanese]

    SAKAI Ko , Ko Sakai

    Journal of the Japanese Society for Artificial Intelligence 5(1), 33-40, 1990-01-01

    J-STAGE  JSAI  Cited by (2)

  • AI入門-15-定理証明技術  [in Japanese]

    坂井 公 , 田中 裕一

    エレクトロニクス 34(3), p57-61, 1989-03

  • AI入門-14-数学とAI  [in Japanese]

    坂井 公 , 田中 裕一

    エレクトロニクス 34(2), p73-77, 1989-02

  • Knuth-Bendix Algorithm and It's Applications.  [in Japanese]

    坂井 公 , Ko Sakai , 新世代コンピュータ技術開発機構

    コンピュータソフトウェア 4(1), 2-22, 1987

    Cited by (5)

  • Term Rewriting System generator Metis  [in Japanese]

    大須賀 昭彦 , 坂井 公 , 横井 俊夫

    項書換えシステム(TRS)とは,書換え規則の集合のことをいうが,理論面で,代数的仕様記述や関数型プログラミング言語にモデルを与えたり,等式を含んだ定理の証明に応用されたりしている他,実用面では,これに基くプログラミング言語や,定理証明システム等もいくつか提案され,理論・実用の両面からその有効性が確認されてきている.ICOTでは,知的プログラミングシステム構築活動の一環としてTRSワーキンググループ …

    全国大会講演論文集 第33回(パターン処理および人工知能), 1425-1426, 1986-10-01

    IPSJ 

  • 人工知能におけるアルゴリズム (最近のアルゴリズム特集) -- (情報・システム)  [in Japanese]

    横井 俊夫 , 坂井 公 , 横田 一正

    The Journal of the Institute of Electronics and Communication Engineers of Japan 69(4), p317-324, 1986-04

  • 超数学と言語 (ゲ-デル<特集>)  [in Japanese]

    坂井 公

    数理科学 23(12), p33-38, 1985-12

    Cited by (1)

  • 論理プログラミング--PROLOGと論理 (応用論理<特集>)  [in Japanese]

    坂井 公

    数理科学 22(11), p9-14, 1984-11

  • INCORPORATING NAIVE NEGATION INTO PROLOG

    Sakai K. , Miyachi T.

    RIMS Kokyuroku (511), 223-241, 1984-02

    IR 

  • 正規論理とそのmodelについて(計算機構に関する数学的基礎理論とその応用)  [in Japanese]

    Sakai Ko

    RIMS Kokyuroku (494), 215-222, 1983-06

    IR 

Page Top