JPS62214432A - 論理型言語処理装置 - Google Patents
論理型言語処理装置Info
- Publication number
- JPS62214432A JPS62214432A JP61056930A JP5693086A JPS62214432A JP S62214432 A JPS62214432 A JP S62214432A JP 61056930 A JP61056930 A JP 61056930A JP 5693086 A JP5693086 A JP 5693086A JP S62214432 A JPS62214432 A JP S62214432A
- Authority
- JP
- Japan
- Prior art keywords
- predicate
- frame
- selection point
- identifier
- goal
- Prior art date
- Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
- Pending
Links
Landscapes
- Devices For Executing Special Programs (AREA)
- Information Retrieval, Db Structures And Fs Structures Therefor (AREA)
Abstract
(57)【要約】本公報は電子出願前の出願データであるた
め要約のデータは記録されません。
め要約のデータは記録されません。
Description
【発明の詳細な説明】
〔産業上の利用分野〕
本発明は、プロログ（Ｐｒｏｌｏｇ）等の論理型言語を
用いて知識処理、推論処理を行うのに通した論理型言語
処理装置、特にバックトラック方式に関する。
用いて知識処理、推論処理を行うのに通した論理型言語
処理装置、特にバックトラック方式に関する。
論理型言語プロログはバックトラックを用いた非決定的
なプログラムが容易に記述できることで知られている。
なプログラムが容易に記述できることで知られている。
このような例として、家康の息子に関する知識と将軍に
関する知識から家康の息子で将軍になった人物を求める
問題を考える。例えば、よく知られたプロログ記法（ｒ
Ｐｒｏｌｏｇプログラミング」中村克彦訳（マイクロソ
フトウェア））によれば、“信服は家康の息子である”
と“秀忠は家康の息子である”という２つの知識は次の
２つの節で表すことができる。
関する知識から家康の息子で将軍になった人物を求める
問題を考える。例えば、よく知られたプロログ記法（ｒ
Ｐｒｏｌｏｇプログラミング」中村克彦訳（マイクロソ
フトウェア））によれば、“信服は家康の息子である”
と“秀忠は家康の息子である”という２つの知識は次の
２つの節で表すことができる。
息子（家康、°信服）。
息子（家康、秀忠）。
また、“家康は将軍である“、“秀忠は将軍である”と
いう２つの知識は次の２つの節で表すことができる。
いう２つの知識は次の２つの節で表すことができる。
将軍（家康）。
将軍（秀忠）。
さらに、“家康の息子で将軍になった人物Ｘは誰か”と
いう問題は下記の質問節で表すことができる。
いう問題は下記の質問節で表すことができる。
？−息子（家康、Ｘ）、将軍（Ｘ）。
プロログの処理系は質問節が与えられると以下のように
動作する。質問節の各ゴール“息子（家康、Ｘ）”、“
将軍（Ｘ） ”について左から右に述語呼び出しを行
う。ゴール“息子（家康、Ｘ）”の述語呼び出しが行わ
れると同一の述語名を持つ節のうち、先ず上位にある節
“息子（家康、信康）、′が選ばれ、節の先頭のゴール
（以下頭ゴールと呼ぶ）と呼び出し側のゴールとのユニ
フィケーションが試みられる。ユニフィケーションは与
えられた２つのゴールを同一のものにする操作で、この
場合は変数Ｘを信康に置き換えることにより達成される
。２つのゴールが同一のものにできたとき２つのゴール
はユニフィケーションしたという。呼び出し側のゴール
と呼ばれた側の節の頭ゴールとのユニフィケーションが
成功すると、呼ばれた側の節が他のゴールを含んでいれ
ば残りのゴールを左から右に実行する。この場合は呼ば
れた側の節が頭ゴールしか含まないので、呼び出し側の
ゴールと頭ゴールがユニフィケーションした段階で述語
呼び出しを終了する。そして、次に呼び出し側の次のゴ
ール“将軍（Ｘ） ”の述語呼び出しが開始される。
動作する。質問節の各ゴール“息子（家康、Ｘ）”、“
将軍（Ｘ） ”について左から右に述語呼び出しを行
う。ゴール“息子（家康、Ｘ）”の述語呼び出しが行わ
れると同一の述語名を持つ節のうち、先ず上位にある節
“息子（家康、信康）、′が選ばれ、節の先頭のゴール
（以下頭ゴールと呼ぶ）と呼び出し側のゴールとのユニ
フィケーションが試みられる。ユニフィケーションは与
えられた２つのゴールを同一のものにする操作で、この
場合は変数Ｘを信康に置き換えることにより達成される
。２つのゴールが同一のものにできたとき２つのゴール
はユニフィケーションしたという。呼び出し側のゴール
と呼ばれた側の節の頭ゴールとのユニフィケーションが
成功すると、呼ばれた側の節が他のゴールを含んでいれ
ば残りのゴールを左から右に実行する。この場合は呼ば
れた側の節が頭ゴールしか含まないので、呼び出し側の
ゴールと頭ゴールがユニフィケーションした段階で述語
呼び出しを終了する。そして、次に呼び出し側の次のゴ
ール“将軍（Ｘ） ”の述語呼び出しが開始される。
このとき、変数Ｘには前の述語呼び出しで“信康”が代
入されているので、呼び出し側のゴールは“将軍（信康
）”として扱われる。“将軍（信康）”が実行されると
同様にして、始めに節“将軍（家康）、”が選ばれる。
入されているので、呼び出し側のゴールは“将軍（信康
）”として扱われる。“将軍（信康）”が実行されると
同様にして、始めに節“将軍（家康）、”が選ばれる。
この節の頭ゴールと呼び出し側のゴールとば同一のゴー
ルにできないのでユニフィケーションは失敗する。ユニ
フィケーションに失敗すると次の節“将軍（秀忠）、”
が選ばれるがこれも同様に失敗する。そして全ての節が
失敗すると呼び出し側のゴール“将軍（信康）”が失敗
となり、バックトラックが引き起こされる。バックトラ
ックが生じると変数Ｘは再び未定義状態に戻されたのち
、前のゴール“息子（家康、Ｘ）”がもう一度実行され
、今度は節“息子（家康、秀忠）、”が選ばれる。そし
て、同様にしてＸに“秀忠”が代入され。今度はゴール
“将軍（秀忠）”として実行される。このゴールに対し
ては、節“将軍（秀忠）。
ルにできないのでユニフィケーションは失敗する。ユニ
フィケーションに失敗すると次の節“将軍（秀忠）、”
が選ばれるがこれも同様に失敗する。そして全ての節が
失敗すると呼び出し側のゴール“将軍（信康）”が失敗
となり、バックトラックが引き起こされる。バックトラ
ックが生じると変数Ｘは再び未定義状態に戻されたのち
、前のゴール“息子（家康、Ｘ）”がもう一度実行され
、今度は節“息子（家康、秀忠）、”が選ばれる。そし
て、同様にしてＸに“秀忠”が代入され。今度はゴール
“将軍（秀忠）”として実行される。このゴールに対し
ては、節“将軍（秀忠）。
”があるので述語呼び出しは成功する。そして、質問節
の全てのゴールが成功してプログラムの実行は終了する
。
の全てのゴールが成功してプログラムの実行は終了する
。
バックトラックはこのように非決定的な処理を実現する
のに有効である。しかしながら、実用的な問題は常に非
決定的な処理を必要とする訳ではなく、唯１つの解のみ
を求めれば良い問題もある。
のに有効である。しかしながら、実用的な問題は常に非
決定的な処理を必要とする訳ではなく、唯１つの解のみ
を求めれば良い問題もある。
例えば、要素が与えられたリストの中に含まれているか
否かをチェックする述語ｍｅｍｂｅｒはＰｒｏ １０ｇ
で次のように書ける。
否かをチェックする述語ｍｅｍｂｅｒはＰｒｏ １０ｇ
で次のように書ける。
ｍｅｍｂｅｒ （Ｘ、 （Ｘ Ｉ Ｙ） ） 。
ｍｅｍｂｅｒ （Ｘ、 （Ｙ Ｉ Ｚ） ） ：
−ｍｅｍｂｅｒ （Ｘ、 Ｚ）ここで、ｍｅｍｂ
ｅｒ （ａ、 （ａ、 ｂ、 ｃ） ）を実行す
ると最初のクローズによりこのゴールは成功する。
−ｍｅｍｂｅｒ （Ｘ、 Ｚ）ここで、ｍｅｍｂ
ｅｒ （ａ、 （ａ、 ｂ、 ｃ） ）を実行す
ると最初のクローズによりこのゴールは成功する。
このとき、次のゴールが失敗したとすると第２クローズ
が代替解として残っているのでバックトラックとして、
残りのリストの中にａがあるかどうかをチェックしよう
とする。しかしながら、与えられたリストの中にａが入
っていたことはすでに一度チェックしているので、残り
のリストの中にａが含まれていることをチェックするの
は明らかに冗長である。
が代替解として残っているのでバックトラックとして、
残りのリストの中にａがあるかどうかをチェックしよう
とする。しかしながら、与えられたリストの中にａが入
っていたことはすでに一度チェックしているので、残り
のリストの中にａが含まれていることをチェックするの
は明らかに冗長である。
ｐｒｏｌｏｇではこのような冗長なバックトラックを除
去するためにカットオペレータ（！で示す）が導入され
ている。カットオペレータは実行されると、その述語の
残りの選択点を除去する働きをする。例えば、ｍｅｍｂ
ｅｒの例はカットオペレータを用いて以下のように記述
すれば、冗長なバ・７クトラツクをしないように定義で
きる。。
去するためにカットオペレータ（！で示す）が導入され
ている。カットオペレータは実行されると、その述語の
残りの選択点を除去する働きをする。例えば、ｍｅｍｂ
ｅｒの例はカットオペレータを用いて以下のように記述
すれば、冗長なバ・７クトラツクをしないように定義で
きる。。
ｍｅｍｂｅｒ （Ｘ、 （Ｘ Ｉ Ｙ） ） ：
ｉ。
ｉ。
ｍｅｍｂｅｒ （Ｘ、 （Ｙ Ｉ Ｚ） ） ：
−ｍｅｍｂｅｒ （Ｘ、 Ｚ）〔発明が解決しよう
とする問題点〕 上記に示したようなカットオペレーションはその有効範
囲が手続きの中に限られるため、プログラム変換でクロ
ーズの一部を展開したりする操作が行いにくいという問
題点がある。例えば、カットがなければ次のように、本
体部にＯＲゴールにで示される）を含むクローズはＯＲ
ゴールを含まないクローズ群に展開してもプログラムの
意味は変わらない。
−ｍｅｍｂｅｒ （Ｘ、 Ｚ）〔発明が解決しよう
とする問題点〕 上記に示したようなカットオペレーションはその有効範
囲が手続きの中に限られるため、プログラム変換でクロ
ーズの一部を展開したりする操作が行いにくいという問
題点がある。例えば、カットがなければ次のように、本
体部にＯＲゴールにで示される）を含むクローズはＯＲ
ゴールを含まないクローズ群に展開してもプログラムの
意味は変わらない。
（ＰＬ）ＯＲゴールを持つクローズ
ｐ： Ｑ＋ （ｒ；ｓ、ｔ）。
ｐニーｕ、ｗ。
（Ｐ２）ＯＲゴールを持たない（ＰＬ）の展開形ｐニー
ｑ、ｄ。
ｑ、ｄ。
ｐニーｕ、ｗ。
ｄニーｒ。
ｄ ニーｓ、ｔ。
しかしながら、（Ｐ３）のように展開されるゴール群の
中にカットオペレータが含まれている場合は（Ｐ４）の
ように展開するとプログラムの意味が変わってしまう。
中にカットオペレータが含まれている場合は（Ｐ４）の
ように展開するとプログラムの意味が変わってしまう。
（Ｐ３）ＯＲゴール内にカットを持つクローズｐ ：
−ｑ、 （ｒ、！ ； ｓ、ｔ）。
−ｑ、 （ｒ、！ ； ｓ、ｔ）。
ｐニーｕ、ｗ。
（Ｐ４）ＯＲゴールを持たない（Ｐ３）の展開形ｐニー
ｑ、ｄ。
ｑ、ｄ。
ｐニーｕ、ｗ。
ｄニーｒ、ｊ。
ｄニーｓ、ｔ。
すなわち、（Ｐ３）のプログラムではＱ＋’が成功する
とｐの選択点がカントされるが、（Ｐ４）ではｑ＋ｒが
成功してもｄの選択点しかカットされず、ｐの選択点は
残ってしまう。
とｐの選択点がカントされるが、（Ｐ４）ではｑ＋ｒが
成功してもｄの選択点しかカットされず、ｐの選択点は
残ってしまう。
本発明の目的は、このような問題点を解決した論理型言
語処理装置を提供することにある。
語処理装置を提供することにある。
本発明の論理型言語処理装置は、代替解を求めるための
バックトラック情報とこのバックトラック情報を生成し
た述語の識別子を格納する選択点フレームと述語の識別
子を格納する述語識別子フレームをリンクで結んで管理
する制御スタックと、代替解を持つ述語が呼ばれた際に
前記選択点フレームを生成して前記制御スタックのリン
クの最後に付け加える選択点フレーム生成手段と、述語
識別子を鍵として選択点フレームを検索し、この選択点
フレームを同一の述語識別子を持つ述語識別子フレーム
に置き換え、この述語識別子フレームをリンクの最後の
フレームとする選択点フレームカット手段と、述語呼び
出しが失敗したときに前記制御スタックのリンクの最後
のフレームからたどって最初の選択点フレームのバック
トラック情報を用いてバックトラックするバックトラッ
ク実行手段とを備え、述語識別子によりカットする選択
点フレームを指定できることを特徴としている。
バックトラック情報とこのバックトラック情報を生成し
た述語の識別子を格納する選択点フレームと述語の識別
子を格納する述語識別子フレームをリンクで結んで管理
する制御スタックと、代替解を持つ述語が呼ばれた際に
前記選択点フレームを生成して前記制御スタックのリン
クの最後に付け加える選択点フレーム生成手段と、述語
識別子を鍵として選択点フレームを検索し、この選択点
フレームを同一の述語識別子を持つ述語識別子フレーム
に置き換え、この述語識別子フレームをリンクの最後の
フレームとする選択点フレームカット手段と、述語呼び
出しが失敗したときに前記制御スタックのリンクの最後
のフレームからたどって最初の選択点フレームのバック
トラック情報を用いてバックトラックするバックトラッ
ク実行手段とを備え、述語識別子によりカットする選択
点フレームを指定できることを特徴としている。
従来のカットオペレータの問題点は、カットオペレータ
の範囲が指定できないことに起因している。この問題は
選択点をカントしたい範囲が述語名で指定可能なラベル
付カットオペレータを用いることによりＩＷ決される。
の範囲が指定できないことに起因している。この問題は
選択点をカントしたい範囲が述語名で指定可能なラベル
付カットオペレータを用いることによりＩＷ決される。
例えば（Ｐ３）の例では、以下の（Ｐ５）のように、述
語ｐの選択点までをカットすることをｃｕｔ（ｐｌｏ）
で明示的に示せば、以下の（Ｐ６）のようにＯＲゴール
を持たないクローズに展開してもプログラムの意味は変
わらない。
語ｐの選択点までをカットすることをｃｕｔ（ｐｌｏ）
で明示的に示せば、以下の（Ｐ６）のようにＯＲゴール
を持たないクローズに展開してもプログラムの意味は変
わらない。
（Ｐ５）ラベル付カットオペレータをＯＲゴール内に持
つクローズ ｐ ニーｑ＋ （ｒ、ｃｕｔ （ｐｌｏ）； ｓ、
む）。
つクローズ ｐ ニーｑ＋ （ｒ、ｃｕｔ （ｐｌｏ）； ｓ、
む）。
ｐニーｕ、ｗ。
（Ｐ６）ＯＲゴールを持たない（Ｐ５）の展開形ｐ ニ
ー（１，ｄ。
ー（１，ｄ。
ｐ： −ｕ、ｗ。
ｄ ： −ｒ、 ｃｕｔ （ｐ／ ｏ） 。
ｄニーｓ、ｔ。
以下、本発明の実施例を図面を用いて詳述する。
第１図は本発明の一実施例である論理型言語処理装置の
機能ブロックレ１である。第１図に図示された論理型言
語処理装置は、選択点フレーム、述語識別子フレームを
保持する制御スタック１００と、呼び出した述語が代替
解を持つ際に選択点フレームを制御スタック１００上に
生成する選択点フレーム生成手段１１０と、述語識別子
を用いて選択点フレームをカントし、述語識別子フレー
ムに置き換える選択点フレームカット手段１２０と、制
御スタック１００上の最後の選択点フレームを用いてバ
ックトラック処理を行うバックトラック実行手段１３０
と、図示されていない他のスタックや入出力装置を用い
てｐｒｏｌｏｇプログラムの実行に必要なユニフィケー
ション処理、入出力処理ならびに算術演算等の処理を行
う処理ユニット１４０と、制御スタック１００２選択点
フレーム生成手段１１０１選択点フレームカット手段１
２０、バックトラック実行手段１３０．処理ユニ・７ト
１４０を結ぶ内部バス１５０と、制御スタック１００に
格納された選択点フレーム、述語識別子フレームのリン
クの最後を保持するリンクレジスタ１６０より構成され
る。・ 本実施例は、例えば以下の（Ｐ７）のプログラムが与え
られると次のように動作する。
機能ブロックレ１である。第１図に図示された論理型言
語処理装置は、選択点フレーム、述語識別子フレームを
保持する制御スタック１００と、呼び出した述語が代替
解を持つ際に選択点フレームを制御スタック１００上に
生成する選択点フレーム生成手段１１０と、述語識別子
を用いて選択点フレームをカントし、述語識別子フレー
ムに置き換える選択点フレームカット手段１２０と、制
御スタック１００上の最後の選択点フレームを用いてバ
ックトラック処理を行うバックトラック実行手段１３０
と、図示されていない他のスタックや入出力装置を用い
てｐｒｏｌｏｇプログラムの実行に必要なユニフィケー
ション処理、入出力処理ならびに算術演算等の処理を行
う処理ユニット１４０と、制御スタック１００２選択点
フレーム生成手段１１０１選択点フレームカット手段１
２０、バックトラック実行手段１３０．処理ユニ・７ト
１４０を結ぶ内部バス１５０と、制御スタック１００に
格納された選択点フレーム、述語識別子フレームのリン
クの最後を保持するリンクレジスタ１６０より構成され
る。・ 本実施例は、例えば以下の（Ｐ７）のプログラムが与え
られると次のように動作する。
（Ｐ７）
ｐニーｑ、ｒ。
ｐニーｓ。
ｑニーｔ、ｕ。
ｔ ： −ｃｕｔ （ｑｌｏ）＋ Ｗ。
ｔ。
？−ｐ。
第２図（１）〜（４）は（Ｐ７）のプログラムを実行し
たときの制御スタック１００およびリンクレジスタ１６
０の変化を示す概念図である。はじめに、質問節により
述語ｐが呼ばれると述語ｐは代替解を持つので選択点フ
レーム生成手段１１Ｏにより述語識別子ｐ１０ （ｏは
引数の個数を表す）を持つ選択点フレーム２１０が生成
され、リンクレジスタ１６０は選択点フレーム２１０を
指す（第２図（１））。
たときの制御スタック１００およびリンクレジスタ１６
０の変化を示す概念図である。はじめに、質問節により
述語ｐが呼ばれると述語ｐは代替解を持つので選択点フ
レーム生成手段１１Ｏにより述語識別子ｐ１０ （ｏは
引数の個数を表す）を持つ選択点フレーム２１０が生成
され、リンクレジスタ１６０は選択点フレーム２１０を
指す（第２図（１））。
次に、述語ｑ、ｔが呼ばれると同様にして選択点フレー
ム２２０，２３０が生成され、リンクレジスタ１６０は
選択点フレーム２３０を措す（第２図（２）、（３’）
）。次に、ｃｕｔ（ｑｌｏ）が実行されると、選択点フ
レームカット手段１２０により識別子ｑ１０を持つ選択
点フレーム２２０が探され、選択点フレーム２２０は同
一の述語識別子を持つ述語識別子フレーム２４０に置換
され、リンクレジスタ１６０は述語識別子フレーム２４
０を指す（第２図（４））。
ム２２０，２３０が生成され、リンクレジスタ１６０は
選択点フレーム２３０を措す（第２図（２）、（３’）
）。次に、ｃｕｔ（ｑｌｏ）が実行されると、選択点フ
レームカット手段１２０により識別子ｑ１０を持つ選択
点フレーム２２０が探され、選択点フレーム２２０は同
一の述語識別子を持つ述語識別子フレーム２４０に置換
され、リンクレジスタ１６０は述語識別子フレーム２４
０を指す（第２図（４））。
そして、この状態でゴールＷが失敗したとするとハック
トラック実行手段１３０によりリンクレジスタ１６０か
ら［旨される最初の選択点フレーム２１０に格納された
バックトラック情報を用いてバックトラックし、次にｐ
の代替解が求められる。
トラック実行手段１３０によりリンクレジスタ１６０か
ら［旨される最初の選択点フレーム２１０に格納された
バックトラック情報を用いてバックトラックし、次にｐ
の代替解が求められる。
以上の動作により、カットしたい範囲を述語名で指定し
て選択点をカットするカットオペレータが実現される。
て選択点をカットするカットオペレータが実現される。
本発明によれば、カットする範囲を述語名で指定して選
択点をカットすることにより従来手法では困難であった
高度なプロログプログラムの実行制御が実現できるとい
う効果がある。
択点をカットすることにより従来手法では困難であった
高度なプロログプログラムの実行制御が実現できるとい
う効果がある。
第１図は本発明の一実施例を示す機能ブロック図、
第２図は第１図で使用する制御スタックの例を示す概念
図である。 １００・・・・制御スタック １１０・・：・選択点フレーム生成手段１２０・・・・
選択点フレームカット手段１３０・・・・バックトラッ
ク実行手段１４０・・・・処理ユニット １５０・・・・内部バス。 １６０・・・・リンクレジスタ
図である。 １００・・・・制御スタック １１０・・：・選択点フレーム生成手段１２０・・・・
選択点フレームカット手段１３０・・・・バックトラッ
ク実行手段１４０・・・・処理ユニット １５０・・・・内部バス。 １６０・・・・リンクレジスタ
Claims (1)
- （１）代替解を求めるためのバックトラック情報とこの
バックトラック情報を生成した述語の識別子を格納する
選択点フレームと述語の識別子を格納する述語識別子フ
レームをリンクで結んで管理する制御スタックと、代替
解を持つ述語が呼ばれた際に前記選択点フレームを生成
して前記制御スタックのリンクの最後に付け加える選択
点フレーム生成手段と、述語識別子を鍵として選択点フ
レームを検索し、この選択点フレームを同一の述語識別
子を持つ述語識別子フレームに置き換え、この述語識別
子フレームをリンクの最後のフレームとする選択点フレ
ームカット手段と、述語呼び出しが失敗したときに前記
制御スタックのリンクの最後のフレームからたどって最
初の選択点フレームのバックトラック情報を用いてバッ
クトラックするバックトラック実行手段とを備え、述語
識別子によりカットする選択点フレームを指定できるこ
とを特徴とする論理型言語処理装置。
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| JP61056930A JPS62214432A (ja) | 1986-03-17 | 1986-03-17 | 論理型言語処理装置 |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| JP61056930A JPS62214432A (ja) | 1986-03-17 | 1986-03-17 | 論理型言語処理装置 |
Publications (1)
| Publication Number | Publication Date |
|---|---|
| JPS62214432A true JPS62214432A (ja) | 1987-09-21 |
Family
ID=13041225
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| JP61056930A Pending JPS62214432A (ja) | 1986-03-17 | 1986-03-17 | 論理型言語処理装置 |
Country Status (1)
| Country | Link |
|---|---|
| JP (1) | JPS62214432A (ja) |
-
1986
- 1986-03-17 JP JP61056930A patent/JPS62214432A/ja active Pending
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| Armstrong | Making reliable distributed systems in the presence of software errors | |
| Shapiro | Algorithmic program debugging | |
| Randell | System structure for software fault tolerance | |
| Mayr | Decidability and complexity of model checking problems for infinite-state systems | |
| Ancona et al. | Comparing trace expressions and linear temporal logic for runtime verification | |
| Summers et al. | Actor services: Modular verification of message passing programs | |
| Melis et al. | Analogy in inductive theorem proving | |
| JP2752094B2 (ja) | 論理型言語におけるバックトラック処理方式 | |
| Futo et al. | The application of PROLOG to the development of QA and DBM systems | |
| Friedman et al. | A polynomial time algorithm for deciding the equivalence problem for 2-tape deterministic finite state acceptors | |
| Clark | Parallel logic programming | |
| Sere et al. | Data refinement of remote procedures | |
| Haridi et al. | An OR-Parallel Token Machine | |
| Ábrahám et al. | Inductive proof outlines for monitors in java | |
| Altisen et al. | Squeezing streams and composition of self-stabilizing algorithms | |
| Loia et al. | High‐level management of computation history for the design and implementation of a prolog system | |
| Ábrahám | A Hoare logic for monitors in Java | |
| JPS62216043A (ja) | 論理型言語処理装置 | |
| Dams | Comparing abstraction refinement algorithms | |
| Gallouzi et al. | An expressive trace theory for LOTOS. | |
| Johnsen et al. | Validating behavioral component interfaces in rewriting logic | |
| Denker et al. | Specifying a reliable broadcasting protocol in Maude | |
| Heinlein | Advanced thread synchronization in Java using interaction expressions | |
| Abrahám et al. | A deductive proof system for multithreaded Java with exceptions | |
| Vediramana Krishnan | Towards Scalable Fully Automatic Program Verification |