【課題】整合性の検査対象であるケースの整合性を自動的に検査することができる整合性検査装置を提供する。
【解決手段】目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部１１と、検査対象情報に対して証明検査を行う検査部１２と、検査部１２による証明検査の結果を出力する検査結果出力部１３と、を備える。

【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、整合性の検査対象であるケースの整合性を検査する整合性検査装置等に関する。
【背景技術】
【０００２】
プラントや飛行機、鉄道、大組織の情報処理システム等のシステムが問題なく動くように設計・構築されることは重要である。しかしながら、そのような複雑なシステムでは、場合分けの数が非常に多くなることがあり、また、各動作等の項目同士が複雑に絡まり合うことがある。したがって、そのような複雑なシステムでは、期待される動作を網羅したのかどうかを確かめることが難しいこともあった。その結果、そのシステムを問題なく設計・構築することは、困難な課題であった。一方、膨大な数の項目のうち、たった一つに関する異常を見落とすことにより、その影響がシステム全体に及び、人命や組織に甚大な影響を及ぼす可能性があるという問題もあった。
【０００３】
近年、そのようなシステムに関して、ありうる問題と、その問題への対処とを共有するための文書として、アシュランス・ケース（ａｓｓｕｒａｎｃｅ ｃａｓｅ）と呼ばれる形式の文書を作成することが行われてきている。そのアシュランス・ケースは、システムの信頼性や安全性等の検討結果を示す文書である。したがって、上述したシステムに関する課題は、アシュランス・ケースに関する正確性の課題に帰着する。なお、構造を明示することによって、アシュランス・ケースを厳密かつ明快に記述する方法として、ＧＳＮ（Ｇｏａｌ Ｓｔｒｕｃｔｕｒｉｎｇ Ｎｏｔａｔｉｏｎ）という方法が用いられている。そのＧＳＮでは、アシュランス・ケースを、ゴール（Ｇｏａｌ）、ストラテジ（Ｓｔｒａｔｅｇｙ）、エビデンス（Ｅｖｉｄｅｎｃｅ）、コンテキスト（Ｃｏｎｔｅｘｔ）、未達成ゴール（Ｕｎｄｅｖｅｌｏｐｅｄ Ｇｏａｌ）であるノードをつないだ有向非巡回グラフの構造で記述する（例えば、非特許文献１参照）。
【先行技術文献】
【非特許文献】
【０００４】
【非特許文献１】Ｔｉｍ Ｋｅｌｌｙ，Ｒｏｂ Ｗｅａｖｅｒ、「Ｔｈｅ Ｇｏａｌ Ｓｔｒｕｃｔｕｒｉｎｇ Ｎｏｔａｔｉｏｎ−Ａ Ｓａｆｅｔｙ Ａｒｇｕｍｅｎｔ Ｎｏｔａｔｉｏｎ」、Ｉｎ ＤＳＮ−２００４：Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ Ｄｅｐｅｎｄａｂｌｅ Ｓｙｓｔｅｍｓ ａｎｄ Ｎｅｔｗｏｒｋｓ ２００４ Ｗｏｒｋｓｈｏｐ ｏｎ Ａｓｓｕｒａｎｃｅ Ｃａｓｅｓ、２００４年
【発明の概要】
【発明が解決しようとする課題】
【０００５】
しかしながら、アシュランス・ケースは、通常、何万ページにもなる膨大な文書であり、文書の整合性があちらこちらで破れてしまうことがあった。また、その整合性の検査を人手で行うのは非常に困難である。さらに、アシュランス・ケースは前述のように、プラントや飛行機等の種々のものを対象とするため、一のアシュランス・ケースを検査するための専用のソフトウェアを開発したとしても、それによって他のアシュランス・ケースを検査できないこともある。そのような場合には、アシュランス・ケースの対象ごとに検査のソフトウェアを開発する必要があり、コストが多大になる。また、アシュランス・ケースの表記方法が変更された場合には、それに応じて、その検査のためのソフトウェアも変更しなければならないという問題もある。
一般的に言えば、アシュランス・ケースのような整合性の検査対象であるケースの整合性を、汎用性の高い方法で精度よく自動的に検査することが求められていた。
【０００６】
本発明は、上記課題を解決するためになされたものであり、整合性の検査対象であるケースの整合性を自動的に検査することができる整合性検査装置等を提供することを目的とする。
【課題を解決するための手段】
【０００７】
上記目的を達成するため、本発明による整合性検査装置は、目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部と、検査対象情報に対して証明検査を行う検査部と、検査部による証明検査の結果を出力する検査結果出力部と、を備えたものである。
このような構成により、整合性の検査対象であるケースを人工言語によって記述することにより、証明検査によって自動的に検査することができるようになる。したがって、検査対象が膨大な量であったとしても、その検査を容易に行うことができる。また、その検査を証明検査、すなわち、定理証明支援系によるプルーフチェッカーによる検査によって行うため、検査のためのソフトウェアを独自に開発する必要もなく、汎用性の高い方法で検査を行うことができる。
【０００８】
また、本発明による整合性検査装置では、検査対象情報は、検査対象情報に含まれる各項の定義を含むモデル情報と、検査対象情報に対応する有向非巡回グラフの構造を示す議論構造情報とを有してもよい。
【０００９】
また、本発明による整合性検査装置では、検査対象情報に対応する有向非巡回グラフの各ノードと、ノード間の親子関係とを示す情報であり、整合性の検査対象であるケースの情報であるグラフ情報が記憶されるグラフ記憶部と、グラフ情報の各ノードの親子関係のパターンに応じて、グラフ情報の各ノードを項に変換し、各ノードの親子関係を演算子に変換し、変換後の検査対象情報を検査対象記憶部に蓄積する翻訳部と、をさらに備えてもよい。
このような構成により、グラフを用いて記述されたケースを検査対象情報に変換し、証明検査を行うことができるようになる。したがって、例えば、人工言語に不慣れな者であっても、人工言語よりも扱いやすいグラフを用いて整合性の検査対象であるケースを記述することによって、そのケースに応じた証明検査の結果を得ることができるようになる。
【００１０】
また、本発明による整合性検査装置では、有向非巡回グラフには、整合性の検査対象であるケースに関する文脈情報に対応するコンテキストノードがさらに含まれ、検査対象情報に対応する有向非巡回グラフの各ノードと、ノード間の親子関係とを示す情報であり、整合性の検査対象であるケースの情報であるグラフ情報が記憶されるグラフ記憶部と、検査対象情報を、項と演算子とのパターンに応じて、検査対象情報の各項をノードに変換し、各演算子を各ノードの親子関係に変換し、変換後のグラフ情報をグラフ記憶部に蓄積する翻訳部と、をさらに備えてもよい。
このような構成により、検査対象情報をグラフ情報に変換することができる。したがって、人工言語で記述されたケースを、視覚的に理解しやすいグラフ情報で見ることができるようになる。
【００１１】
また、本発明による整合性検査装置では、人工言語は、構成的型理論に基づく人工言語であってもよい。
このような構成により、その人工言語で記述されたケース自体をプログラムとして実行することもできるようになる。
【００１２】
また、本発明による整合性検査装置では、検査部による証明検査によって、エラーのないことが検査された検査対象情報を実行する実行部をさらに備えてもよい。
【００１３】
また、本発明による整合性検査装置では、実行部は、検査対象情報を実行することにより、検査対象情報から、整合性の検査対象であるケースの各ノードに応じた項と、各ノードの親子関係に応じた演算子とを陽に記述する形式の検査対象情報を生成してもよい。
このような構成により、翻訳の前に、あるいは、翻訳中に、検査対象情報を項や演算子を陽に記述した形式に変換することによって、検査対象情報をグラフ情報に変換することができるようになる。
【００１４】
また、本発明による整合性検査装置では、検査対象記憶部では、検査対象情報をグラフ情報に変換する処理に応じた変換プログラムも記憶され、翻訳部は、変換プログラムを実行することによって、検査対象情報をグラフ情報に変換してもよい。
このような構成により、その変換プログラムによって、翻訳部による情報の変換が実現されるようになる。
【００１５】
また、本発明による整合性検査装置では、検査対象情報と変換プログラムとは、構成的型理論に基づく同じ人工言語で記述されていてもよい。
このような構成により、変換プログラム自体についても、証明検査の対象とすることができ、検査済の変換プログラムによって、変換の処理を行うことができるようになる。
【００１６】
また、本発明による整合性検査装置では、検査対象情報の項は、メタ変数を含むものであり、人工言語は、対話型証明支援系の人工言語であってもよい。
このような構成により、メタ変数を含む検査対象情報（例えば、作成途中の検査対象情報）であっても、その段階で証明検査を行うことができる。その結果、その段階において、検査対象情報が適切に構成されているかどうかを確認することができる。
【発明の効果】
【００１７】
本発明による整合性検査装置等によれば、アシュランス・ケースなどの整合性の検査対象であるケースの整合性を、証明検査によって検査することができる。したがって、汎用性の高い方法によって精度よく自動的に検査することができる。
【図面の簡単な説明】
【００１８】
【図１】本発明の実施の形態１による整合性検査装置の構成を示すブロック図
【図２】同実施の形態による整合性検査装置の動作を示すフローチャート
【図３】同実施の形態による整合性検査装置の動作を示すフローチャート
【図４】同実施の形態による整合性検査装置の動作を示すフローチャート
【図５】同実施の形態による整合性検査装置の動作を示すフローチャート
【図６】同実施の形態による整合性検査装置の動作を示すフローチャート
【図７】同実施の形態による整合性検査装置の動作を示すフローチャート
【図８】同実施の形態による整合性検査装置の動作を示すフローチャート
【図９】同実施の形態におけるケース及びアーギュメントの構造について説明するための図
【図１０】同実施の形態における検査対象情報の一例を示す図
【図１１】同実施の形態におけるグラフ情報の表示の一例を示す図
【図１２Ａ】同実施の形態におけるグラフ情報の一例を示す図
【図１２Ｂ】同実施の形態におけるグラフ情報の一例を示す図
【図１３】同実施の形態における検査対象情報の一例を示す図
【図１４】同実施の形態におけるグラフ情報の表示の一例を示す図
【図１５】同実施の形態における検査対象情報の一例を示す図
【図１６】同実施の形態におけるグラフ情報の表示の一例を示す図
【図１７Ａ】同実施の形態における検査対象情報の一例を示す図
【図１７Ｂ】同実施の形態における検査対象情報の一例を示す図
【図１８】同実施の形態における検査対象情報の一例を示す図
【図１９】同実施の形態におけるグラフ情報の表示の一例を示す図
【図２０】同実施の形態における検査対象情報に取り込まれる情報の一例を示す図
【図２１Ａ】同実施の形態における検査対象情報の一例を示す図
【図２１Ｂ】同実施の形態における検査対象情報の一例を示す図
【図２２】同実施の形態におけるグラフ情報の表示の一例を示す図
【図２３】同実施の形態における検査対象情報に取り込まれる情報の一例を示す図
【図２４】同実施の形態における検査対象情報の一例を示す図
【図２５】同実施の形態におけるエラーの表示の一例を示す図
【図２６】同実施の形態における検査対象情報の一例を示す図
【図２７】同実施の形態におけるグラフ情報の表示の一例を示す図
【図２８】同実施の形態における検査対象情報の一例を示す図
【図２９】同実施の形態におけるグラフ情報の表示の一例を示す図
【図３０】同実施の形態における検査対象情報の一例を示す図
【図３１】同実施の形態におけるグラフ情報の表示の一例を示す図
【図３２】同実施の形態における検査対象情報の一例を示す図
【図３３】同実施の形態におけるグラフ情報の表示の一例を示す図
【図３４】同実施の形態における検査対象情報の一例を示す図
【図３５】同実施の形態におけるエラーの表示の一例を示す図
【図３６】同実施の形態におけるグラフ情報の表示の一例を示す図
【図３７】同実施の形態における検査対象情報の一例を示す図
【図３８】同実施の形態におけるエラーの表示の一例を示す図
【図３９】同実施の形態におけるコンピュータシステムの外観一例を示す模式図
【図４０】同実施の形態におけるコンピュータシステムの構成の一例を示す図
【発明を実施するための形態】
【００１９】
以下、本発明による整合性検査装置について、実施の形態を用いて説明する。なお、以下の実施の形態において、同じ符号を付した構成要素及びステップは同一または相当するものであり、再度の説明を省略することがある。
【００２０】
（実施の形態１）
本発明の実施の形態１による整合性検査装置について、図面を参照しながら説明する。本実施の形態による整合性検査装置は、人工言語で記述された、整合性の検査対象であるケースに対して、証明検査を行うことによって、そのケースの整合性を検査する。
【００２１】
図１は、本実施の形態による整合性検査装置１の構成を示すブロック図である。本実施の形態による整合性検査装置１は、検査対象記憶部１１と、検査部１２と、検査結果出力部１３と、実行部１４と、グラフ記憶部１５と、翻訳部１６と、表示部１７と、受付部１８とを備える。
【００２２】
検査対象記憶部１１では、検査対象情報が記憶される。検査対象情報は、整合性の検査対象であるケースを、証明検査の対象となる人工言語により記述した情報である。整合性の検査対象であるケースは、例えば、前述のアシュランス・ケースやセーフティー・ケースなどであってもよく、それ以外のケースであってもよい。そのケースは、複数のノードを含む有向非巡回グラフの構造を有するものである。その構造に現れ得る複数のノードの種類には、少なくとも、目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとが含まれる。その複数のノードには、整合性の検査対象であるケースに関する文脈情報に対応するコンテキストノードがさらに含まれてもよい。また、その複数のノードには、証明がまだなされていない未達成ゴールがさらに含まれてもよい。本実施の形態では、整合性の検査対象であるケースが、ゴールノード、ストラテジノード、エビデンスノード、及び、コンテキストノードを有する場合について主に説明する。有向非巡回グラフの構造に含まれる各ノードは、有向非巡回グラフの構造を有するように接続されているため、各ノードは、単数または複数の親ノードを有することになる。但し、非巡回であるため、親の方向、または、子の方向にノードをたどった場合に、元のノードに戻ることはないものとする。その有向非巡回グラフの構造では、ルートノードが単数であってもよく、または、複数であってもよい。本実施の形態の以下の説明では、有向非巡回グラフのルートノードが単数であるとする。なお、ルートノードが単数でない有向非巡回グラフは、通常、ルートノードが単数である複数の有向非巡回グラフに分けて考えることが可能である。ルートノードが複数である有向非巡回グラフは、ルートノードが単数である２以上の有向非巡回グラフの組み合わせであると考えることもできる。また、そのルートノードが単数である有向非巡回グラフは、例えば、木構造であってもよく、または、そうでなくてもよい。木構造である場合には、各ノードは、単数の親ノードを有することになる。本実施の形態では、有向非巡回グラフが木構造である場合について主に説明する。その有向非巡回グラフは、ルートノードであるゴールノード（このゴールノードを「トップゴールノード」と呼ぶこともある）を、単数または複数の他のゴールノード（このゴールノードを「サブゴールノード」と呼ぶこともある）に分解し、リーフノードであるエビデンスノードに至るものである。ＧＳＮで知られているように、通常、トップゴールノードが複数のサブゴールノードに分解され、それが繰り返されて、最終的に最もリーフ側のサブゴールノードがエビデンスノードによって証明されることになる。したがって、各サブゴールノードが証明されたことになり、その結果、トップゴールノードが証明されたことになる。なお、通常、単数のゴールノードが、複数のゴールノードに分解される際に、ストラテジノードによって分解されることになる。また、エビデンスノードに至るリーフ側の構造が確定されていないゴールノードは、未達成ゴールノードとなる。また、整合性の検査対象であるケース全体の文脈情報、または、そのケースの一部の文脈情報が、コンテキストノードにより示される。
【００２３】
検査対象情報は、その複数のノードを含む有向非巡回グラフの構造を有するケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報である。また、その検査対象情報は、前述のように、証明検査の対象となる人工言語により記述された情報である。その人工言語は、証明検査を行うことができる人工言語である。また、その人工言語は、構成的型理論に基づく人工言語であってもよく、または、そうでなくてもよい。本実施の形態では、その人工言語が構成的型理論に基づく人工言語である場合について主に説明する。そのような人工言語として、例えば、ＡｇｄａやＣｏｑ、ＮｕＰＲＬ等が知られている。本実施の形態では、構成的型理論に基づく人工言語がＡｇｄａである場合について主に説明する。また、検査対象情報は、検査対象情報に含まれる各項の定義を含むモデル情報と、検査対象情報に対応する有向非巡回グラフの構造を示す議論構造情報とを有する情報であってもよい。本実施の形態では、主にその場合について説明する。議論構造情報は、整合性の検査対象であるケースにおける各ノードの親子関係を人工言語によって記述した情報である。モデル情報は、例えば、そのモデル情報の全部が議論構造情報に含まれない情報であってもよく、そのモデル情報の全部が議論構造情報に含まれてもよく、または、そのモデル情報の一部が議論構造情報に含まれてもよい。以下、モデル情報のうち、議論構造情報に含まれる情報を局所モデル情報と呼び、議論構造情報に含まれない情報を大局モデル情報と呼ぶこともある。したがって、モデル情報は、そのすべてが大局モデル情報であってもよく、そのすべてが局所モデル情報であってもよく、または、大局モデル情報と局所モデル情報とを含んでいてもよい。また、検査対象情報に含まれる議論構造情報は、具体的な有向非巡回グラフの構造に応じた議論構造情報の生成関数（生成プログラム）と、引数の値とを含む情報であってもよい。その場合には、議論構造情報そのものによっては、ノードの具体的な親子関係が示されないが、その議論構造情報に含まれる引数の値を、その議論構造情報に含まれる生成関数に適用して、その生成関数を実行することによって、具体的な有向非巡回グラフの構造に応じた議論構造情報が生成されることになるため、実質的に、ノードの具体的な親子関係を示す議論構造情報が与えられた場合と同様であると考えることができる。その具体的な有向非巡回グラフの構造に応じた議論構造情報とは、整合性の検査対象であるケースの各ノードに応じた項と、各ノードの親子関係に応じた演算子とを陽に記述する形式の議論構造情報である。なお、その生成関数の実行は、実行部１４によって行われる。また、検査対象情報には、証明検査において用いる情報に関する実行プログラムが含まれていてもよい。その場合には、証明検査が行われる際に、その実行プログラムが実行され、その実行結果を用いて証明検査が行われることになる。その実行結果は、例えば、その時点で得られた情報であってもよく、または、その他の情報であってもよい。具体的には、その実行プログラムが実行されることによって、その時点における値（例えば、温度や圧力、センサの値等）が取得され、それを用いて証明検査が行われることになってもよい。なお、その実行プログラムの実行は、実行部１４によって行われる。
【００２４】
ここで、検査対象情報によって記述されるケースの構造について簡単に説明する。図９（ａ）で示されるように、一のケースは、ルートノードであるゴールノードと、そのゴールノードの子である部分木構造であるアーギュメントとを有するか、または、ゴールノードをルートノードとする部分ケースと、そのゴールノードを親とするコンテキストノードとを有する。なお、アーギュメントは、図９（ｂ）で示されるように、ルートノードであるストラテジノードと、そのストラテジノードの子である１以上のケースとを有するか、エビデンスノードそのものであるか、または、ストラテジノードをルートノードとする部分アーギュメントと、そのストラテジノードを親とするコンテキストノードとを有する。なお、子ノードであるケースを有しないストラテジノードは、エビデンスノードと同じであるが、本実施の形態では、そのようなストラテジノードをエビデンスノードとして扱う。整合性の検査対象となるケースは図９で示される構造を有しているため、前述のように、ゴールノードと、ストラテジノードと、エビデンスノードと、コンテキストノードとの親子関係によって記述することができる。なお、図９では、ケースが木構造である場合について説明したが、前述のように、ケースは有向非巡回グラフであってもよい。したがって、その場合には、例えば、エビデンスノードが２以上の親ノードを有してもよい。
【００２５】
次に、図９で示されるケースを構成的型理論に基づく人工言語であるＡｇｄａにより記述する場合における検査対象情報について、拡張バッカス・ナウア記法（Ｅｘｔｅｎｄｅｄ Ｂａｃｋｕｓ−Ｎａｕｒ Ｆｏｒｍ、ＥＢＮＦ；ＩＳＯ／ＩＥＣ １４９７７：１９９６）に準じた記法を用いて説明する。ケース、アーギュメント、ゴール、ストラテジ、エビデンス、コンテキストそれぞれのＡｇｄａ表記の範疇を、Ｃａｓｅ，Ａｒｇｕｍｅｎｔ，Ｇｏａｌ，Ｓｔｒａｔｅｇｙ，Ｅｖｉｄｅｎｃｅ，Ｃｏｎｔｅｘｔと表記するものとする。すると、図９（ａ）に対応して、Ｃａｓｅは次のように記述される。
【００２６】
Ｃａｓｅ：：＝Ｇｏａｌ∋Ａｒｇｕｍｅｎｔ
｜ＣＯＮＴＥＸＴ［Ｃｏｎｔｅｘｔ／Ｃａｓｅ］
【００２７】
なお、「：：＝」は、左辺の範疇のものは右辺のように構成されることを示すＥＢＮＦの記法であり、「｜」は、「または」を示す記法である。上の式の場合、一のＣａｓｅは、一のＧｏａｌ「ｇ」と一のＡｒｇｕｍｅｎｔ「ａ」から「ｇ∋ａ」として構成されるか、または、一のＣｏｎｔｅｘｔ「ｓ」と一のＣａｓｅ「ｄ」から「ＣＯＮＴＥＸＴ［ｓ／ｄ］」として構成されるかであることを示している。また、図９（ｂ）に対応して、Ａｒｇｕｍｅｎｔは次のように記述される。
【００２８】
Ａｒｇｕｍｅｎｔ：：＝Ｓｔｒａｔｅｇｙ｛・Ｃａｓｅ｝
｜Ｅｖｉｄｅｎｃｅ
｜ＣＯＮＴＥＸＴ［Ｃｏｎｔｅｘｔ／Ａｒｇｕｍｅｎｔ］
【００２９】
ここで、｛ ｝は、０以上の繰り返しを示すＥＢＮＦの記法である。また、「∋」、「・」、またはＣＯＮＴＥＸＴ［ ／ ］は、演算子である。また、Ｇｏａｌ，Ｓｔｒａｔｅｇｙ，Ｅｖｉｄｅｎｃｅ，Ｃｏｎｔｅｘｔは項である。したがって、各ノードの親子関係で示されるケースと、そのケースを人工言語で記述した検査対象情報とは、上述のようにして対応付けられるため、任意のケースを人工言語（この場合にはＡｇｄａ）を用いて記述することができるようになる。
【００３０】
また、上述した各演算子の定義について簡単に説明する。まず、「∋」のＡｇｄａでの定義は次の二行のようになる。
＿∋＿：（Ａ：Ｓｅｔ）→（ａ：Ａ）→Ａ
Ａ∋ａ＝ａ
【００３１】
したがって、Ａｇｄａ表記「Ａ∋ａ」は、「ａ」と同じ値を指し示しつつ、ａの型がＡであることを明示する表記となる。なお、この演算子「∋」の定義を言葉で説明すると、「第一引数Ａが型、第二引数ａがＡ型のときに限り型検査に通り、その場合（Ａ型の）ａを値として返す演算子」であると言うことができる。したがって、Ａｇｄａ以外の構成的型理論に基づく人工言語において「∋」と同様の演算子を定義する際には、そのような性質を有する演算子を定義すればよい。
【００３２】
次に、「・」のＡｇｄａでの定義は次の二行のようになる。
＿・＿：｛Ａ：Ｓｅｔ｝→｛Ｂ：Ａ→Ｓｅｔ｝→（ｆ：（ａ：Ａ）→Ｂａ）→（ａ：Ａ）→Ｂａ
ｆ・ａ＝ｆａ
【００３３】
したがって、Ａｇｄａ表記「ｆ・ａ」は、「ｆａ」（関数ｆに引数ａを適用した結果）と同じ値を指し示しつつ、関数部分と引数部分の別を明示する表記となる。なお、この演算子「・」の定義を言葉で説明すると、「第一引数ｆが関数であって、その関数の型を（ｘ：Ａ）→Ｂｘとして、第二引数ａがＡ型のときに限り型検査に通り、その場合（Ｂａ型の）ｆａを値として返す演算子」であると言うことができる。したがって、Ａｇｄａ以外の構成的型理論に基づく人工言語において「・」と同様の演算子を定義する際には、そのような性質を有する演算子を定義すればよい。
【００３４】
次に、ＣＯＮＴＥＸＴ［ｓ／ｘ］は、ケースｘやアーギュメントｘに文脈情報（文字列）ｓを追加する演算子である。したがって、ＣＯＮＴＥＸＴ［ｓ／ｘ］はｘである。したがって、Ａｇｄａ以外の構成的型理論に基づく人工言語においてＣＯＮＴＥＸＴ［ ／ ］と同様の演算子を定義する際には、そのような性質を有する演算子を定義すればよい。
【００３５】
検査対象記憶部１１に検査対象情報が記憶される過程は問わない。例えば、記録媒体を介して検査対象情報が検査対象記憶部１１で記憶されるようになってもよく、通信回線等を介して送信された検査対象情報が検査対象記憶部１１で記憶されるようになってもよく、入力デバイスを介して入力された検査対象情報が検査対象記憶部１１で記憶されるようになってもよく、あるいは、翻訳部１６がグラフ情報を変換した検査対象情報が検査対象記憶部１１で記憶されるようになってもよい。検査対象記憶部１１での記憶は、ＲＡＭ等における一時的な記憶でもよく、あるいは、長期的な記憶でもよい。検査対象記憶部１１は、所定の記録媒体（例えば、半導体メモリや磁気ディスク、光ディスクなど）によって実現されうる。
【００３６】
検査部１２は、検査対象情報に対して証明検査を行う。この証明検査は、証明検査を行う人工言語においてあらかじめ用意されているものである。この検査部１２は、そのような人工言語においてプルーフチェッカー（ｐｒｏｏｆ ｃｈｅｃｋｅｒ）と呼ばれる機能によって実現される。検査部１２は、証明検査によって、エラーの有無を取得することができる。また、検査部１２は、エラーが存在する場合に、そのエラーの箇所を示す情報をも取得してもよい。エラーの箇所を示す情報は、例えば、検査対象情報における行番号であってもよく、それにコラム番号が加わったものであってもよく、基準となる位置からの文字数やデータ容量（例えば、バイト数等）であってもよく、または、それらの組み合わせであってもよい。なお、この検査部１２の機能は、前述のように、プルーフチェッカーとして公知であり、その詳細な説明を省略する。
【００３７】
検査結果出力部１３は、検査部１２による証明検査の結果を出力する。証明検査の結果は、例えば、エラーの有無を示す情報を含んでいてもよく、エラーが存在する場合に、そのエラーの箇所を示す情報を含んでいてもよく、または、その他の証明検査の結果を含んでいてもよい。証明検査の結果によりエラーの箇所を示す場合には、例えば、行番号やコラム番号等が表示されることによって、エラーの箇所が特定できるようにされてもよく、ハイライト表示（例えば、下線や太字等の強調表示がなされたり、他の部分と色が変更されたりしてもよい）によってエラーの箇所が示されてもよく、エラーの箇所の先頭にカーソルを移動させることによってエラーの箇所が示されてもよく、あるいは、その他の方法によってエラーの箇所が示されてもよい。ここで、この出力は、例えば、表示デバイス（例えば、ＣＲＴや液晶ディスプレイなど）への表示でもよく、所定の機器への通信回線を介した送信でもよく、プリンタによる印刷でもよく、スピーカによる音声出力でもよく、記録媒体への蓄積でもよく、他の構成要素への引き渡しでもよい。なお、検査結果出力部１３は、出力を行うデバイス（例えば、表示デバイスやプリンタなど）を含んでもよく、あるいは含まなくてもよい。また、検査結果出力部１３は、ハードウェアによって実現されてもよく、あるいは、それらのデバイスを駆動するドライバ等のソフトウェアによって実現されてもよい。
【００３８】
実行部１４は、検査部１２による証明検査によって、エラーのないことが検査された検査対象情報を実行する。その検査対象情報の実行は、例えば、後述する検査対象情報からグラフ情報への変換の際に行われる。検査対象情報からグラフ情報への変換の際に検査対象情報が実行される場合には、実行部１４は、前述のように、生成関数と引数の値とを含む議論構造情報において、その引数の値をその生成関数に適用して実行することにより、ノードの具体的な親子関係を示す議論構造情報、すなわち、整合性の検査対象であるケースの各ノードに応じた項と、各ノードの親子関係に応じた演算子とを陽に記述する形式の議論構造情報を生成してもよい。この生成関数の実行は、検査対象情報からグラフ情報への変換の際に行われるものである。その生成関数の実行は、例えば、検査対象情報からグラフ情報への変換の際に、一括して行われてもよく、または、変換の処理の進行に応じて、逐次的に行われてもよい。いずれの場合であっても、実行部１４は、ノードの具体的な親子関係を示す議論構造情報を生成するための実行を少なくとも行えばよく、それ以上の実行を行わなくてもよい。
【００３９】
なお、実行部１４は、検査部１２による証明検査の際に検査対象情報を実行してもよい。前述のように、検査対象情報に、証明検査において用いる情報に関する実行プログラムが含まれている場合には、実行部１４は、その検査対象情報の証明検査が行われる際に、その実行プログラムを実行し、その実行結果を検査部１２に渡してもよい。そして、検査部１２において、その実行結果を用いて証明検査が行われることになる。
【００４０】
グラフ記憶部１５では、グラフ情報が記憶される。グラフ情報は、検査対象情報に対応する有向非巡回グラフの各ノードと、それらの間の親子関係とを示す情報である。また、グラフ情報は、整合性の検査対象であるケースの情報である。前述の検査対象情報は、人工言語で記述されたものであるため、不慣れな者には理解しにくいことがあるが、このグラフ情報は、ノードの親子関係を視覚的に知ることができる情報であるため、専門家でなくても理解しやすい情報である。このグラフ情報は、各ノードの性質を示す情報（例えば、各ノードがゴールノードであるのか、ストラテジノードであるのか、エビデンスノードであるのかなどを示す情報）と、その各ノードの親子関係を示す情報を含む情報であればよい。したがって、グラフ情報は、例えば、各ノードの情報と、そのノードの親子関係を示すリンク情報とを有する情報であってもよく、親のノードを示す情報を含む各ノードの情報であってもよく、子のノードを示す情報を含む各ノードの情報であってもよい。このように、グラフ情報の構造は問わない。また、グラフ情報は、例えば、ＸＭＬのようにマークアップ言語で記述されるものであってもよく、または、その他のデータ形式の情報であってもよい。
【００４１】
グラフ記憶部１５にグラフ情報が記憶される過程は問わない。例えば、記録媒体を介してグラフ情報がグラフ記憶部１５で記憶されるようになってもよく、通信回線等を介して送信されたグラフ情報がグラフ記憶部１５で記憶されるようになってもよく、入力デバイスを介して入力されたグラフ情報がグラフ記憶部１５で記憶されるようになってもよく、あるいは、翻訳部１６が検査対象情報を変換したグラフ情報がグラフ記憶部１５で記憶されるようになってもよい。グラフ記憶部１５での記憶は、ＲＡＭ等における一時的な記憶でもよく、あるいは、長期的な記憶でもよい。グラフ記憶部１５は、所定の記録媒体（例えば、半導体メモリや磁気ディスク、光ディスクなど）によって実現されうる。
【００４２】
翻訳部１６は、検査対象情報と、グラフ情報との間の変換を行う。翻訳部１６は、例えば、検査対象情報をグラフ情報に変換し、変換後のグラフ情報をグラフ記憶部１５に蓄積してもよく、グラフ情報を検査対象情報に変換し、変換後の検査対象情報を検査対象記憶部１１に蓄積してもよく、または、その両方の処理を行ってもよい。本実施の形態では、翻訳部１６がその両方の処理を行う場合について主に説明する。検査対象情報をグラフ情報に変換する場合には、翻訳部１６は、検査対象情報を、項と演算子とのパターンに応じて、検査対象情報の各項をノードに変換し、各演算子を各ノードの親子関係に変換する。また、グラフ情報を検査対象情報に変換する場合には、翻訳部１６は、グラフ情報の各ノードの親子関係のパターンに応じて、グラフ情報の各ノードを項に変換し、各ノードの親子関係を演算子に変換する。なお、翻訳部１６による変換の処理の詳細については、フローチャートを用いて後述する。
【００４３】
表示部１７は、検査対象記憶部１１で記憶されている検査対象情報や、グラフ記憶部１５で記憶されているグラフ情報を表示する。なお、検査対象情報を表示する際には、表示部１７は、その検査対象情報をそのまま表示すればよい。一方、グラフ情報を表示する際には、表示部１７は、そのグラフ情報を各ノードの親子関係が分かる有向非巡回グラフの画像を生成して、その画像を表示してもよく、あるいは、グラフ情報をそのまま表示してもよい。なお、ノードと、そのノードの親子関係を示す情報から有向非巡回グラフの画像を生成する方法はすでに公知であり、その詳細な説明を省略する。また、表示部１７は、その他の情報を表示してもよい。例えば、実行部１４による実行の結果を表示してもよい。なお、表示部１７は、それらの表示を行う表示デバイス（例えば、ＣＲＴや液晶ディスプレイなど）を含んでもよく、あるいは含まなくてもよい。また、表示対象の表示は、別の装置においてなされてもよい。その場合には、表示部１７は、装置の外部に対して表示対象の情報を送信するものであってもよい。また、表示部１７は、ハードウェアによって実現されてもよく、あるいは表示デバイスを駆動するドライバ等のソフトウェアによって実現されてもよい。
【００４４】
受付部１８は、指示や情報を受け付ける。例えば、受付部１８は、検査対象情報に関する受け付けを行い、それに応じて、検査対象記憶部１１で記憶されている検査対象情報を変更してもよい。また、例えば、受付部１８は、グラフ情報に関する受け付けを行い、それに応じて、グラフ記憶部１５で記憶されているグラフ情報を変更してもよい。また、例えば、受付部１８は、検査の指示や翻訳の指示を受け付け、それに応じて、検査部１２や翻訳部１６に対して、検査や翻訳を行う旨の指示を渡してもよい。
【００４５】
なお、受付部１８が受け付けた情報に応じてグラフ記憶部１５で記憶されているグラフ情報を変更し、その変更後のグラフ情報に応じたノードとリンクとを表示部１７が表示するシステムとして、Ｄ−Ｃａｓｅ Ｅｄｉｔｏｒが知られている。したがって、グラフ情報の変更や、グラフ情報の表示に関する詳細な説明は省略する。そのＤ−Ｃａｓｅ Ｅｄｉｔｏｒの詳細については、例えば、次のＵＲＬを参照されたい。なお、Ｄ−Ｃａｓｅの「Ｄ」は、Ｄｅｐｅｎｄａｂｉｌｉｔｙを示す。
ＵＲＬ：ｈｔｔｐ：／／ｗｗｗ．ｉｌ．ｉｓ．ｓ．ｕ−ｔｏｋｙｏ．ａｃ．ｊｐ／ｄｅｏｓ／ｄｃａｓｅ／Ｄ−Ｃａｓｅ＿Ｅｄｉｔｏｒ．ｈｔｍｌ
【００４６】
受付部１８は、例えば、入力デバイス（例えば、キーボードやマウス、タッチパネルなど）から入力された情報を受け付けてもよく、有線もしくは無線の通信回線を介して送信された情報を受信してもよく、所定の記録媒体（例えば、光ディスクや磁気ディスク、半導体メモリなど）から読み出された情報を受け付けてもよい。なお、受付部１８は、受け付けを行うためのデバイス（例えば、モデムやネットワークカードなど）を含んでもよく、あるいは含まなくてもよい。また、受付部１８は、ハードウェアによって実現されてもよく、あるいは所定のデバイスを駆動するドライバ等のソフトウェアによって実現されてもよい。
【００４７】
なお、検査対象記憶部１１と、グラフ記憶部１５とは、同一の記録媒体によって実現されてもよく、あるいは、別々の記録媒体によって実現されてもよい。前者の場合には、検査対象情報を記憶している領域が検査対象記憶部１１となり、グラフ情報を記憶している領域がグラフ記憶部１５となる。
【００４８】
次に、整合性検査装置１の動作について図２のフローチャートを用いて説明する。
（ステップＳ１０１）検査部１２は、証明検査を行うかどうか判断する。そして、証明検査を行う場合には、ステップＳ１０２に進み、そうでない場合には、ステップＳ１０４に進む。なお、検査部１２は、例えば、検査の指示が受付部１８で受け付けられた場合に、検査を行うと判断してもよく、または、その他のタイミングで検査を行うと判断してもよい。
【００４９】
（ステップＳ１０２）検査部１２は、検査対象記憶部１１で記憶されている検査対象情報について証明検査を行う。そして、その検査結果を取得する。
【００５０】
（ステップＳ１０３）検査結果出力部１３は、検査部１２による検査結果を出力する。そして、ステップＳ１０１に戻る。
【００５１】
（ステップＳ１０４）受付部１８は、検査対象情報に関する情報を受け付けたかどうか判断する。そして、検査対象情報に関する情報を受け付けた場合には、ステップＳ１０５に進み、そうでない場合には、ステップＳ１０７に進む。
【００５２】
（ステップＳ１０５）受付部１８は、受け付けた検査対象情報に関する情報に応じて、検査対象記憶部１１で記憶されている検査対象情報を変更する。その変更は、例えば、検査対象情報の蓄積であってもよく、検査対象情報の削除であってもよく、検査対象情報の一部の変更であってもよい。
【００５３】
（ステップＳ１０６）表示部１７は、変更後の検査対象情報を表示する。そして、ステップＳ１０１に戻る。
【００５４】
（ステップＳ１０７）受付部１８は、グラフ情報に関する情報を受け付けたかどうか判断する。そして、グラフ情報に関する情報を受け付けた場合には、ステップＳ１０８に進み、そうでない場合には、ステップＳ１１０に進む。
【００５５】
（ステップＳ１０８）受付部１８は、受け付けたグラフ情報に関する情報に応じて、検査対象記憶部１１で記憶されているグラフ情報を変更する。その変更は、例えば、グラフ情報の蓄積であってもよく、グラフ情報の削除であってもよく、グラフ情報の一部の変更であってもよい。
【００５６】
（ステップＳ１０９）表示部１７は、変更後のグラフ情報を表示する。そして、ステップＳ１０１に戻る。
【００５７】
（ステップＳ１１０）翻訳部１６は、検査対象情報をグラフ情報に変換するかどうか判断する。そして、その変換を行う場合には、ステップＳ１１１に進み、そうでない場合には、ステップＳ１１３に進む。なお、翻訳部１６は、例えば、検査対象情報からグラフ情報への変換の指示が受付部１８で受け付けられた場合に、その変換を行うと判断してもよく、または、その他のタイミングでその変換を行うと判断してもよい。
【００５８】
（ステップＳ１１１）翻訳部１６は、検査対象情報をグラフ情報に変換する。その変換の詳細な処理については、図３のフローチャートを用いて後述する。
【００５９】
（ステップＳ１１２）表示部１７は、変換後のグラフ情報を表示する。そして、ステップＳ１０１に戻る。
【００６０】
（ステップＳ１１３）翻訳部１６は、グラフ情報を検査対象情報に変換するかどうか判断する。そして、その変換を行う場合には、ステップＳ１１４に進み、そうでない場合には、ステップＳ１０１に戻る。なお、翻訳部１６は、例えば、グラフ情報から検査対象情報への変換の指示が受付部１８で受け付けられた場合に、その変換を行うと判断してもよく、または、その他のタイミングでその変換を行うと判断してもよい。
【００６１】
（ステップＳ１１４）翻訳部１６は、グラフ情報を検査対象情報に変換する。その変換の詳細な処理については、図６のフローチャートを用いて後述する。
【００６２】
（ステップＳ１１５）表示部１７は、変換後の検査対象情報を表示する。そして、ステップＳ１０１に戻る。
【００６３】
なお、図２のフローチャートにおいて、電源オフや処理終了の割り込みにより処理は終了する。また、図２のフローチャートにおいて、検査対象情報をグラフ情報に変換する際には、検査部１２による証明検査によって、問題のないことが確認されているべきである。したがって、ステップＳ１１０からステップＳ１１１に進む際に、証明検査を行い、問題のないことが確認された場合にのみステップＳ１１１に進み、問題がある場合には、ステップＳ１０１に戻るようにしてもよい。
【００６４】
図３は、図２のフローチャートにおける検査対象からグラフへの翻訳の処理（ステップＳ１１１）の詳細を示すフローチャートである。
（ステップＳ２０１）翻訳部１６は、検査対象記憶部１１で記憶されている検査対象情報において、ケースに応じた記述がなされている箇所を特定する。通常、その箇所は、議論構造情報における有向非巡回グラフに対応する範囲である。その記述の箇所の特定は、例えば、その記述の箇所を図示しない記録媒体に蓄積することであってもよく、その特定した箇所にフラグ等を設定することであってもよく、その特定した箇所を示す情報（例えば、行番号やコラム番号等）を図示しない記録媒体に蓄積することであってもよく、あるいは、その他の特定であってもよい。
【００６５】
（ステップＳ２０２）実行部１４は、検査対象情報を実行するかどうか判断する。そして、実行を行う場合には、ステップＳ２０３に進み、そうでない場合には、ステップＳ２０４に進む。なお、実行部１４は、検査対象情報において、ケースが何らかの生成関数を用いて記述されており、項や演算子が陽に記述されていない場合に、検査対象情報を実行すると判断し、そうでない場合に、実行しないと判断してもよい。
【００６６】
（ステップＳ２０３）実行部１４は、検査対象情報を実行する。すなわち、検査対象情報に含まれる生成関数を実行することによって、項や演算子を陽に記述する形式の検査対象情報を生成する。その実行後の検査対象情報は、検査対象記憶部１１に蓄積されてもよい。
【００６７】
（ステップＳ２０４）翻訳部１６は、ステップＳ２０１で特定されたケースに応じた記述の処理、すなわち、そのケースに応じた記述をグラフの情報に変換する処理を行う。この処理の詳細については、図４のフローチャートを用いて後述する。
【００６８】
（ステップＳ２０５）翻訳部１６は、グラフ記憶部１５で記憶されているグラフ情報に、ノード等を追加する処理を行うかどうか判断する。そして、ノード等を追加する処理を行う場合には、ステップＳ２０６に進み、そうでない場合には、図２のフローチャートに戻る。なお、翻訳部１６は、例えば、検査対象情報にモデル情報が含まれる場合に、ノード等を追加する処理を行うと判断してもよく、議論構造情報にノードの親子関係以外を示す情報が含まれる場合に、ノード等を追加する処理を行うと判断してもよく、あるいは、その他の場合に、ノード等を追加する処理を行うと判断してもよい。
【００６９】
（ステップＳ２０６）翻訳部１６は、グラフ記憶部１５で記憶されているグラフ情報に、ノード等の情報を追加する。そして、図２のフローチャートに戻る。なお、具体的には、翻訳部１６は、モデル情報やケース名等に対応したコンテキストノードをグラフ情報に追加してもよく、モデル情報に対応した情報をグラフ情報に追加してもよく、または、その他の情報をグラフ情報に追加してもよい。なお、ノード以外の情報が追加された場合には、グラフ情報が表示される際に、その追加された情報が表示されなくてもよい。すなわち、グラフ情報は、検査対象情報の少なくとも一部の情報を、不可視情報として有してもよい。
【００７０】
図３のフローチャートでは、ステップＳ２０３において実行部１４が生成関数を実行することにより、検査対象情報を一括して項や演算子を陽に記述する形式に変換する場合について説明したが、そうでなくてもよい。例えば、前述のように、翻訳の処理において逐次的にその変換を行ってもよい。また、図３のフローチャートでは、翻訳部１６が、検査対象情報をグラフ情報に変換した情報を逐次、グラフ記憶部１５に蓄積するものとするが、そうでなくてもよい。翻訳部１６は、図示しない記録媒体に順次、グラフ情報の一部の情報を蓄積し、グラフ情報が完成した後に、それをグラフ記憶部１５に一括して蓄積してもよい。
【００７１】
図４は、図３のフローチャートにおけるケースに応じた記述の処理（ステップＳ２０４）の詳細を示すフローチャートである。
（ステップＳ３０１）翻訳部１６は、処理の対象となるケースのパターンを特定する。図９（ａ）で示されるように、これは通常、ゴールとアーギュメントのパターンか、あるいは、ケースとコンテキストのパターンとなる。このパターンの特定は、あらかじめ図示しない記録媒体で記憶されているパターンを読み出し、そのパターンマッチングにより行うことができる。そのパターンは、例えば、「ｇ∋ｔ１」や、「ＣＯＮＴＥＸＴ［ｓ／ｔ２］」のパターンである。ｇは任意のゴールの項であり、ｔ１は任意のアーギュメントであり、ｔ２は任意のケースであり、ｓは任意のコンテキストの項である。
【００７２】
（ステップＳ３０２）翻訳部１６は、特定したパターンに応じたノードを生成する。例えば、パターン「ｇ∋ｔ」を特定した場合には、翻訳部１６は、それに応じて「ｇ」に対応するゴールノードを生成する。また、例えば、パターン「ＣＯＮＴＥＸＴ［ｓ／ｔ］」を特定した場合には、翻訳部１６は、それに応じて「ｓ」に対応するコンテキストノードを生成する。
【００７３】
（ステップＳ３０３）翻訳部１６は、ステップＳ３０２で生成した以外の残りの部分は、ケースであるかどうか判断する。例えば、パターン「ｇ∋ｔ」を特定した場合には、翻訳部１６は、「ｇ」に対応するゴールノード以外の残りの部分がケースではないアーギュメント「ｔ」であると判断する。一方、例えば、パターン「ＣＯＮＴＥＸＴ［ｓ／ｔ］」を特定した場合には、翻訳部１６は、「ｓ」に対応するコンテキストノード以外の残りの部分がケース「ｔ」であると判断する。そして、残りの部分がケースである場合には、ステップＳ３０４に進み、そうでない場合には、ステップＳ３０５に進む。
【００７４】
（ステップＳ３０４）翻訳部１６は、その残りの部分について、ケースに応じた記述の処理を実行する。その処理は、図４のフローチャートで示されるものである。すなわち、翻訳部１６は、ケースに応じた記述の処理を再帰的に実行することになる。
【００７５】
（ステップＳ３０５）翻訳部１６は、その残りの部分について、アーギュメントに応じた記述の処理を実行する。その処理の詳細については、図５のフローチャートを用いて後述する。
【００７６】
（ステップＳ３０６）翻訳部１６は、ステップＳ３０２で生成したノードと、その残りの部分とのリンクを生成する。そのリンクの向きは、ステップＳ３０１で特定したパターンに応じたものとなる。そして、上位のフローチャートに戻る。例えば、パターン「ｇ∋ｔ」を特定した場合には、翻訳部１６は、「ｇ」に対応するゴールノードが親となり、「ｔ」に対応するアーギュメントのルートノードが子となるリンクを生成する。また、例えば、パターン「ＣＯＮＴＥＸＴ［ｓ／ｔ］」を特定した場合には、翻訳部１６は、「ｓ」に対応するコンテキストノードが子となり、残りのケース「ｔ」のルートノード（ゴールノード）が親となるリンクを生成する。
【００７７】
図５は、図４のフローチャートにおけるアーギュメントに応じた記述の処理（ステップＳ３０５）の詳細を示すフローチャートである。
（ステップＳ４０１）翻訳部１６は、処理の対象となるアーギュメントのパターンを特定する。図９（ｂ）で示されるように、これは通常、ストラテジとケースのパターンか、エビデンスのパターンか、あるいは、アーギュメントとコンテキストのパターンとなる。このパターンの特定は、あらかじめ図示しない記録媒体で記憶されているパターンを読み出し、そのパターンマッチングにより行うことができる。そのパターンは、例えば、「ｆ・ｔ_１・ｔ_２・…・ｔ_ｎ」や、「ＣＯＮＴＥＸＴ［ｓ／ｔ］」のパターンである。前者のパターンで、ｎが１以上の場合には、ｆは、任意のストラテジの項であり、ｔ_１等は、任意のケースに応じた項であり、ｎが０の場合には、ｆは、任意のエビデンスの項である。また、後者のパターンの場合、ｔは、任意のアーギュメントの項であり、ｓは、任意のコンテキストの項である。
【００７８】
（ステップＳ４０２）翻訳部１６は、特定したパターンに応じたノードを生成する。例えば、ｎ≧１のパターン「ｆ・ｔ_１・ｔ_２・…・ｔ_ｎ」を特定した場合には、翻訳部１６は、それに応じて「ｆ」に対応するストラテジノードを生成する。また、例えば、ｎ＝０のパターン「ｆ・ｔ_１・ｔ_２・…・ｔ_ｎ」を特定した場合には、翻訳部１６は、それに応じて「ｆ」に対応するエビデンスノードを生成する。また、例えば、パターン「ＣＯＮＴＥＸＴ［ｓ／ｔ］」を特定した場合には、翻訳部１６は、それに応じて「ｓ」に対応するコンテキストノードを生成する。
【００７９】
（ステップＳ４０３）翻訳部１６は、生成したノードがリーフノード、すなわち、エビデンスノードであるかどうか判断する。そして、リーフノードである場合には、上位のフローチャートに戻り、そうでない場合には、ステップＳ４０４に進む。
【００８０】
（ステップＳ４０４）翻訳部１６は、ステップＳ４０３で生成した以外の残りの部分は、ケースであるかどうか判断する。例えば、ｎ≧１のパターン「ｆ・ｔ_１・ｔ_２・…・ｔ_ｎ」を特定した場合には、翻訳部１６は、「ｆ」に対応するストラテジノード以外の残りの部分がケース「ｔ_１」、「ｔ_２」、…、「ｔ_ｎ」であると判断する。また、例えば、パターン「ＣＯＮＴＥＸＴ［ｓ／ｔ］」を特定した場合には、翻訳部１６は、「ｓ」に対応するコンテキストノード以外の残りの部分がアーギュメント「ｔ」であると判断する。そして、残りの部分がケースである場合には、ステップＳ４０５に進み、そうでない場合には、ステップＳ４０８に進む。
【００８１】
（ステップＳ４０５）翻訳部１６は、その残りの部分について、ケースに応じた記述の処理を実行する。その処理は、図４のフローチャートで示されるものである。
【００８２】
（ステップＳ４０６）翻訳部１６は、ステップＳ４０２で生成したノードと、その残りの部分とのリンクを生成する。そのリンクの向きは、ステップＳ４０１で特定したパターンに応じたものとなる。そして、上位のフローチャートに戻る。例えば、ｎ≧１のパターン「ｆ・ｔ_１・ｔ_２・…・ｔ_ｎ」を特定した場合には、翻訳部１６は、「ｆ」に対応するストラテジノードが親となり、ステップＳ４０５で処理を行ったケースのルートノード（ゴールノード）が子となるリンクを生成する。
【００８３】
（ステップＳ４０７）翻訳部１６は、まだ処理のなされていないケースが存在するかどうか判断する。そして、存在する場合には、ステップＳ４０５に戻って、そのケースに応じた記述の処理を実行し、そうでない場合には、上位のフローチャートに戻る。なお、ステップＳ４０１において、ｎ≧１のパターン「ｆ・ｔ_１・ｔ_２・…・ｔ_ｎ」が特定された場合には、ステップＳ４０５，Ｓ４０６の処理がｎ回、繰り返されることになる。
【００８４】
（ステップＳ４０８）翻訳部１６は、その残りの部分について、アーギュメントに応じた記述の処理を実行する。その処理は、図５のフローチャートで示されるものである。すなわち、翻訳部１６は、アーギュメントに応じた記述の処理を再帰的に実行することになる。
【００８５】
（ステップＳ４０９）翻訳部１６は、ステップＳ４０２で生成したノードと、その残りの部分とのリンクを生成する。そのリンクの向きは、ステップＳ４０１で特定したパターンに応じたものとなる。そして、上位のフローチャートに戻る。例えば、パターン「ＣＯＮＴＥＸＴ［ｓ／ｔ］」を特定した場合には、翻訳部１６は、「ｓ」に対応するコンテキストノードが子となり、残りのアーギュメント「ｔ」のルートノード（ストラテジノード、または、エビデンスノード）が親となるリンクを生成する。
【００８６】
図６は、図２のフローチャートにおけるグラフから検査対象への翻訳の処理（ステップＳ１１４）の詳細を示すフローチャートである。
（ステップＳ５０１）翻訳部１６は、グラフ記憶部１５で記憶されているグラフ情報において、ルートノードを特定する。本実施の形態では、ルートノードが１個である有向非巡回グラフを扱うため、このルートノードは１個に特定される。なお、ルートノードは、親ノードを有さないノードである。したがって、グラフ情報に含まれるノードやリンクを示す情報を用いて、各ノードに親ノードが存在するかどうか判断し、親ノードが存在しないと判断されたノードがルートノードとなる。なお、ルートノードの特定は、例えば、そのルートノードを識別する情報を図示しない記録媒体に蓄積することであってもよく、そのルートノードに対応付けてフラグ等を設定することであってもよく、あるいは、その他の特定であってもよい。
【００８７】
（ステップＳ５０２）翻訳部１６は、ステップＳ５０１で特定したノードをルートノードとするケースに関する処理を行う。この処理の詳細については、図７のフローチャートを用いて後述する。
【００８８】
（ステップＳ５０３）翻訳部１６は、検査対象情報に追加する情報が存在するかどうか判断する。そして、存在する場合には、ステップＳ５０４に進み、そうでない場合には、図２のフローチャートに戻る。
【００８９】
（ステップＳ５０４）翻訳部１６は、グラフ情報に含まれる情報を検査対象情報に追加する。例えば、グラフ情報に不可視情報が含まれる場合には、その不可視情報に対応するモデル情報を検査対象情報に追加してもよい。また、グラフ情報に、例えば、モデル情報やケース名等に対応したコンテキストノードが含まれる場合には、そのコンテキストノードに含まれるモデル情報やケース名等を検査対象情報に追加してもよい。そして、図２のフローチャートに戻る。
【００９０】
図６のフローチャートでは、翻訳部１６が、グラフ情報を検査対象情報に変換した情報を逐次、検査対象記憶部１１に蓄積するものとするが、そうでなくてもよい。翻訳部１６は、図示しない記録媒体に順次、検査対象情報の一部の情報を蓄積し、検査対象情報が完成した後に、それを検査対象記憶部１１に一括して蓄積してもよい。また、グラフ情報を検査対象情報に翻訳する際には、グラフ情報においてモデル情報に対応する情報が含まれていないこともあり得る。そのような場合には、グラフ情報を、検査対象情報の議論構造情報に対応する部分に翻訳し、その後、検査対象情報において、適宜、モデル情報に対応する情報が追加されてもよい。
【００９１】
図７は、図６のフローチャートにおけるケースの処理（ステップＳ５０２）の詳細を示すフローチャートである。
（ステップＳ６０１）翻訳部１６は、カウンタｉを１に設定する。
【００９２】
（ステップＳ６０２）翻訳部１６は、処理対象となっているケースのルートノードを親とするｉ番目のリンクについて、親子関係のパターンを特定する。図９（ａ）で示されるように、これは通常、親のゴールノードと、子のアーギュメントとのパターンか、親のゴールノードと、子のコンテキストノードとのパターンとなる。なお、子がアーギュメントである場合には、具体的には、子のルートノードは、ストラテジノードかエビデンスノードとなる。このパターンの特定は、あらかじめ図示しない記録媒体で記憶されているパターンを読み出し、そのパターンマッチングにより行うことができる。そのパターンは、例えば、（親ノード、子ノード）が、（ゴールノード、ストラテジノード）であるパターンや、（ゴールノード、エビデンスノード）であるパターン、または、（ゴールノード、コンテキストノード）であるパターンである。
【００９３】
（ステップＳ６０３）翻訳部１６は、ｉ番目のリンクのリンク先がアーギュメントであるかどうか判断する。例えば、ステップＳ６０２でパターン（ゴールノード、ストラテジノード）や、（ゴールノード、エビデンスノード）を特定した場合には、翻訳部１６は、リンク先がアーギュメントであると判断し、ステップＳ６０２でパターン（ゴールノード、コンテキストノード）を特定した場合には、翻訳部１６は、リンク先がコンテキストノードである、すなわち、アーギュメントでないと判断する。そして、リンク先がアーギュメントである場合には、ステップＳ６０４に進み、そうでない場合には、ステップＳ６０５に進む。
【００９４】
（ステップＳ６０４）翻訳部１６は、ｉ番目のリンクのリンク先のノードがルートノードであるアーギュメントに関する処理を行う。この処理の詳細については、図８のフローチャートを用いて後述する。
【００９５】
（ステップＳ６０５）翻訳部１６は、ｉ番目のリンクのリンク先であるコンテキストノードに対応する項を生成する。その項は、演算子ＣＯＮＴＥＸＴ［ｓ／ ］の「ｓ」に対応する項である。
【００９６】
（ステップＳ６０６）翻訳部１６は、ｉ番目のリンクについて特定したパターンに応じた演算子を生成する。例えば、パターン（ゴールノード、ストラテジノード）や、（ゴールノード、エビデンスノード）を特定した場合には、翻訳部１６は、（ゴールノードの項）∋（ストラテジノードをルートノードとするアーギュメントの項）や、（ゴールノードの項）∋（エビデンスノードをルートノードとするアーギュメントの項）となる演算子「∋」を生成する。また、例えば、パターン（ゴールノード、コンテキストノード）を特定した場合には、翻訳部１６は、ＣＯＮＴＥＸＴ［（コンテキストノードの項）／（ゴールノードをルートノードとするケースの項）］となる演算子ＣＯＮＴＥＸＴ［ ／ ］を生成する。
【００９７】
（ステップＳ６０７）翻訳部１６は、カウンタｉを１だけインクリメントする。
【００９８】
（ステップＳ６０８）翻訳部１６は、処理対象となっているケースのルートノードを親とするｉ番目のリンクが存在するかどうか判断する。そして、存在する場合には、ステップＳ６０２に戻り、存在しない場合には、ステップＳ６０９に進む。
【００９９】
（ステップＳ６０９）翻訳部１６は、処理対象となっているケースのルートノードであるゴールノードの項を生成する。
【０１００】
（ステップＳ６１０）翻訳部１６は、ｉ−１個のリンクのうち、リンク先にアーギュメントを持つものが一つだけあり、他は全てリンク先にコンテキスト等の他のノードを持つかどうか判断する。そして、そうである場合には、ステップＳ６１１に進み、そうでない場合には、ステップＳ６１２に進む。
【０１０１】
（ステップＳ６１１）翻訳部１６は、ステップＳ６０４〜Ｓ６０６，Ｓ６０９で生成したアーギュメントの項やリンク先の項、演算子、ルートノードであるゴールノードの項を用いて、処理の対象となっているケースの項を生成する。例えば、非アーギュメントの子が全てコンテキストノードである場合に、翻訳部１６は、ゴールノードをルートノードにもつケースの項として、
ＣＯＮＴＥＸＴ［（コンテキストノードの項１）／
ＣＯＮＴＥＸＴ［（コンテキストノードの項２）／
…
ＣＯＮＴＥＸＴ［（コンテキストノードの項｛ｉ−２｝）／
（ゴールノードの項）∋（アーギュメントの項）
］…］］
を生成する。なお、ここでｉ≧２であり、ｉ＝２の場合には、演算子ＣＯＮＴＥＸＴ［ ／ ］は用いられない。非アーギュメントの子にコンテキストノード以外のものがある場合も、上のＣＯＮＴＥＸＴ［ ／ ］に代えてステップＳ６０６で生成される演算子を用いて、同様にケースの項を生成する。そして、上位フローチャートに戻る。
【０１０２】
（ステップＳ６１２）翻訳部１６は、ケースの構造に合わないグラフが処理されたことを表す「エラーケースの項」を生成する。「エラーケースの項」としては、証明検査の結果が必ずエラーになるものを選ぶ。また、「エラーケースの項」は、エラーを生じたケースのルートノードを指定する情報を参考に含んでいてもよく、それぞれの子の翻訳結果である項を参考に含んでいてもよい。そして、上位フローチャートに戻る。
【０１０３】
なお、ステップＳ６１２において、翻訳部１６は、ケースの構造に合わないグラフが処理されたことの警告を出力してもよく、また、上位のフローチャートの処理を含めてステップＳ１１４を異常終了してもよい。
【０１０４】
図８は、図７のフローチャートにおけるアーギュメントの処理（ステップＳ６０４）の詳細を示すフローチャートである。
（ステップＳ７０１）翻訳部１６は、処理対象となっているアーギュメントのルートノードにリンク先のノードが存在するかどうか判断する。そして、リンク先のノードが存在する場合には、ステップＳ７０２に進み、そうでない場合には、ステップＳ７１０に進む。
【０１０５】
（ステップＳ７０２）翻訳部１６は、カウンタｊを１に設定する。
【０１０６】
（ステップＳ７０３）翻訳部１６は、処理対象となっているアーギュメントのルートノードを親とするｊ番目のリンクについて、親子関係のパターンを特定する。図９（ｂ）で示されるように、これは通常、親のストラテジノードと、子のケースとのパターンか、親のストラテジノードと、子のコンテキストノードとのパターンが、親のエビデンスノードと子のコンテキストノードのパターンとなる。なお、子がケースである場合には、具体的には、子のルートノードはゴールノードとなる。このパターンの特定は、あらかじめ図示しない記録媒体で記憶されているパターンを読み出し、そのパターンマッチングにより行うことができる。そのパターンは、例えば、（親ノード、子ノード）が、（ストラテジノード、ゴールノード）であるパターンや、（ストラテジノード、コンテキストノード）であるパターン、または、（エビデンスノード、コンテキストノード）であるパターンである。
【０１０７】
（ステップＳ７０４）翻訳部１６は、ｊ番目のリンクのリンク先がケースであるかどうか判断する。例えば、ステップＳ７０３でパターン（ストラテジノード、ゴールノード）を特定した場合には、翻訳部１６は、リンク先がケースであると判断し、ステップＳ７０３でパターン（ストラテジノード、コンテキストノード）を特定した場合には、翻訳部１６は、リンク先がコンテキストノードである、すなわち、ケースでないと判断する。そして、リンク先がケースである場合には、ステップＳ７０５に進み、そうでない場合には、ステップＳ７０６に進む。
【０１０８】
（ステップＳ７０５）翻訳部１６は、ｊ番目のリンクのリンク先であるゴールノードがルートノードであるケースに関する処理を行う。その処理は、図７のフローチャートで示されるものである。
【０１０９】
（ステップＳ７０６）翻訳部１６は、ｊ番目のリンクのリンク先が、例えば、コンテキストノードであった場合には、コンテキストノードに対応する項を生成する。その項は、演算子ＣＯＮＴＥＸＴ［ｓ／ ］の「ｓ」に対応する項である。
【０１１０】
（ステップＳ７０７）翻訳部１６は、ｊ番目のリンクについて特定したパターンに応じた演算子を生成する。例えば、パターン（ストラテジノード、ゴールノード）を特定した場合には、翻訳部１６は、（ストラテジノードの項）・（ゴールノードをルートノードとするケースの項）となる演算子「・」を生成する。また、例えば、パターン（ストラテジノード、コンテキストノード）を特定した場合には、翻訳部１６は、ＣＯＮＴＥＸＴ［（コンテキストノードの項）／（ストラテジノードをルートノードとするアーギュメントの項）］となる演算子ＣＯＮＴＥＸＴ［ ／ ］を生成する。
【０１１１】
（ステップＳ７０８）翻訳部１６は、カウンタｊを１だけインクリメントする。
【０１１２】
（ステップＳ７０９）翻訳部１６は、処理対象となっているアーギュメントのルートノードを親とするｊ番目のリンクが存在するかどうか判断する。そして、存在する場合には、ステップＳ７０３に戻り、存在しない場合には、ステップＳ７１０に進む。
【０１１３】
（ステップＳ７１０）翻訳部１６は、処理対象となっているアーギュメントのルートノードに応じた項を生成する。例えば、処理対象となっているアーギュメントがエビデンスノードである場合には、エビデンスの項を生成し、処理対象となっているアーギュメントのルートノードがストラテジノードである場合には、そのストラテジノードの項を生成する。
【０１１４】
（ステップＳ７１１）翻訳部１６は、ステップＳ７０５〜Ｓ７０７，Ｓ７１０で生成したケースの項やリンク先の項、演算子、ルートノードの項を用いて、処理の対象となっているアーギュメントの項を生成する。すなわち、翻訳部１６は、処理対象となっているアーギュメントのルートノードにリンクがなかった場合、すなわち、ステップＳ７０１からステップＳ７１０に進んだ場合には、ステップＳ７１０で生成した項そのものをアーギュメントの項とする。一方、処理対象となっているアーギュメントのルートノードにリンクがあった場合には、例えば、翻訳部１６は、さらに、ケースでない子が全てコンテキストノードであったときに、ステップＳ７０５で生成されたケースの項をケース項１、ケース項２、…、ケース項ｋ、ステップＳ７０６で生成されたコンテキストノードの項をコンテキストノード項１、コンテキストノード項２、…、コンテキストノード項ｍとおき（ここで、ｋ、ｍ≧０、ｊ−１＝ｋ＋ｍとなる）、処理対象となっているアーギュメントの項として、
ＣＯＮＴＥＸＴ［（コンテキストノード項１）／
ＣＯＮＴＥＸＴ［（コンテキストノード項２）／
…
ＣＯＮＴＥＸＴ［（コンテキストノード項ｍ）／
（ステップＳ７１０で生成されたストラテジまたはエビデンスの項）
・（ケース項１）
・（ケース項２）
…
・（ケース項ｋ）
］…］］
を生成する。非ケースの子にコンテキストノード以外のものがある場合も、上のＣＯＮＴＥＸＴ［ ／ ］に代えてステップＳ７０７で生成される演算子を用いて、同様にアーギュメントの項を生成する。そして、上位のフローチャートに戻る。
【０１１５】
なお、アーギュメントのルートノードがエビデンスノードであり、かつｋ＞０である場合には、ステップＳ６１２と同様にアーギュメントの構造に合わないグラフが処理されたことを表す「エラーアーギュメントの項」を生成してもよく、または、上位のフローチャートの処理を含めてステップＳ１１４を異常終了してもよい。
【０１１６】
また、図３〜図８のフローチャートを用いて説明した翻訳の処理は一例であり、それ以外の処理によって、検査対象情報をグラフ情報に翻訳してもよく、または、グラフ情報を検査対象情報に翻訳してもよい。また、図３〜図８のフローチャートにおける翻訳の処理は、ケースが木構造を有する場合の処理である。ケースが有向非巡回グラフの構造を有する場合の処理については後述する。
【０１１７】
次に、本実施の形態による整合性検査装置１の動作について、具体例を用いて説明する。この具体例では、構成的型理論に基づく人工言語がＡｇｄａであり、整合性の検査対象がディーケースである場合について説明する。ディーケースは、前述のケースの概念を一部拡張した具体例である。また、この具体例では、整合性の検査対象であるディーケースが、木構造を有する場合について説明する。なお、「ディーケース」概念の本来の表記は「Ｄ−Ｃａｓｅ」であるが、前述の「Ｃａｓｅ」の具体例として次に定義するＤ−Ｃａｓｅとの混乱をさけるため、ここではカナで表記する。
【０１１８】
また、この具体例における記述についてさらに詳細に説明する。Ｄ−Ｃａｓｅ（前述のＣａｓｅ），Ａｒｇｕｍｅｎｔ，Ｇｏａｌ，Ｓｔｒａｔｅｇｙ，Ｅｖｉｄｅｎｃｅは、次のようになる。
Ｄ−Ｃａｓｅ：：＝Ｇｏａｌ∋Ａｒｇｕｍｅｎｔ
｜ＣＯＮＴＥＸＴ［Ｃｏｎｔｅｘｔ／Ｄ−Ｃａｓｅ］
Ａｒｇｕｍｅｎｔ：：＝Ｓｔｒａｔｅｇｙ｛・Ｄ−Ｃａｓｅ｝
｜Ｅｖｉｄｅｎｃｅ
｜ＣＯＮＴＥＸＴ［Ｃｏｎｔｅｘｔ／Ａｒｇｕｍｅｎｔ］
Ｇｏａｌ：：＝ＦｏｒｍａｌＧｏａｌ
｜＜＜ＦｏｒｍａｌＧｏａｌ／Ｄｅｓｃｒｉｐｔｉｏｎ＞＞
Ｓｔｒａｔｅｇｙ：：＝ＦｏｒｍａｌＳｔｒａｔｅｇｙ
｜＜ＦｏｒｍａｌＳｔｒａｔｅｇｙ／Ｄｅｓｃｒｉｐｔｉｏｎ＞
Ｅｖｉｄｅｎｃｅ：：＝ＦｏｒｍａｌＥｖｉｄｅｎｃｅ
｜＜ＦｏｒｍａｌＥｖｉｄｅｎｃｅ／Ｄｅｓｃｒｉｐｔｉｏｎ＞
【０１１９】
なお、Ｃｏｎｔｅｘｔは、Ｄｅｓｃｒｉｐｔｉｏｎである。また、ＦｏｒｍａｌＳｔｒａｔｅｇｙ，ＦｏｒｍａｌＥｖｉｄｅｎｃｅはＡｇｄａ項（Ａｇｄａ言語での式）である。また、ＦｏｒｍａｌＧｏａｌは、Ｓｅｔ型のＡｇｄａ項であり、Ｄｅｓｃｒｉｐｔｉｏｎは、Ｓｔｒｉｎｇ型のＡｇｄａ項である。このように、Ｄｅｓｃｒｉｐｔｉｏｎを記述できることによって、検査対象情報をディーケースのグラフ情報に翻訳した際に、そのＤｅｓｃｒｉｐｔｉｏｎの文字列をノードに対応付けて表示することも可能である。
【０１２０】
この具体例での検査対象情報は、Ｄ−Ｃａｓｅに名称をつける定義を含むことができる。さらに、この定義は、パラメータを含むことができる。定義されたＤ−Ｃａｓｅをその名称で参照できることの効用については、後述する。
この具体例では、Ｄ−Ｃａｓｅの定義を、Ａｇｄａ言語における関数定義の宣言によって行う。後者の一般的な記述は、次のようになる。
ＦｕｎｃｔｉｏｎＤｅｆｉｎｉｔｉｏｎ：：＝［ＴｙｐｅＳｉｇｎａｔｕｒｅ］
ＦｕｎｃｔｉｏｎＣｌａｕｓｅ
｛ＦｕｎｃｔｉｏｎＣｌａｕｓｅ｝
｛Ｐｒａｇｍａ｝
ＴｙｐｅＳｉｇｎａｔｕｒｅ：：＝ＦｕｎｃｔｉｏｎＮａｍｅ：ＡｇｄａＴｙｐｅ
ＦｕｎｃｔｉｏｎＣｌａｕｓｅ
：：＝ＬｅｆｔＨａｎｄＳｉｄｅ＝ＲｉｇｈｔＨａｎｄＳｉｄｅ
ＬｅｆｔＨａｎｄＳｉｄｅ：：＝ＦｕｎｃｔｉｏｎＮａｍｅ｛Ｐａｔｔｅｒｎ｝
Ｐａｔｔｅｒｎ：：＝ＰａｔｔｅｒｎＶａｒｉａｂｌｅ
｜ＣｏｎｓｔｒｕｃｔｏｒＮａｍｅ｛Ｐａｔｔｅｒｎ｝
【０１２１】
ここで、［ ］は、オプションであることを示すＥＢＮＦの表記である。また、ＡｇｄａＴｙｐｅはＳｅｔ型のＡｇｄａ項であり、ＰａｔｔｅｒｎＶａｒｉａｂｌｅは、Ａｇｄａの識別子であり、ＣｏｎｓｔｒｕｃｔｏｒＮａｍｅは、Ａｇｄａのコンストラクター識別子であり、ＲｉｇｈｔＨａｎｄＳｉｄｅは、Ａｇｄａの表現である。ＦｕｎｃｔｉｏｎＤｅｆｉｎｉｔｉｏｎは、ＴｙｐｅＳｉｇｎａｔｕｒｅと、１以上のＦｕｎｃｔｉｏｎＣｌａｕｓｅと、０個以上のＰｒａｇｍａ（プラグマ）とから構成される。ＴｙｐｅＳｉｇｎａｔｕｒｅは、関数名と、その型とを規定する。ＦｕｎｃｔｉｏｎＣｌａｕｓｅから型を推測できるのであれば、そのＴｙｐｅＳｉｇｎａｔｕｒｅは省略してもよい。また、ＦｕｎｃｔｉｏｎＣｌａｕｓｅは、左辺（ＬｅｆｔＨａｎｄＳｉｄｅ）と右辺（ＲｉｇｈｔＨａｎｄＳｉｄｅ）とを等号でつなぐものである。左辺は、０以上のＰａｔｔｅｒｎの適用された関数名である。Ｐａｔｔｅｒｎは、ＰａｔｔｅｒｎＶａｒｉａｂｌｅ（変数）であるか、あるいは、０以上のサブＰａｔｔｅｒｎに適用されたコンストラクター識別子である。右辺は、左辺に現れたＰａｔｔｅｒｎＶａｒｉａｂｌｅの使用されたＡｇｄａ項である。Ｐｒａｇｍａは、関数定義宣言を処理するＡｇｄａ言語処理系に対する指令であり、定義されるところの関数に特定の情報を付帯させるものである。
【０１２２】
この具体例では、整合性の検査対象の概念も、ディーケースの定義を含むよう拡張される。概念自体は、人工言語（Ａｇｄａ）で検査対象情報として記述される以前の情報であるが、含まれるべき情報の構成要素を便宜上ＥＢＮＦ記法で表すと次のようになる。
ディーケース宣言：：＝ＳｉｎｇｌｅＣｌａｕｓｅＤｅｃｌ
ＳｉｎｇｌｅＣｌａｕｓｅＤｅｃｌ
：：＝ＳｉｎｇｌｅＣｌａｕｓｅＳｉｇｎａｔｕｒｅ ディーケース
ＳｉｎｇｌｅＣｌａｕｓｅＳｉｇｎａｔｕｒｅ
：：＝ＤＣａｓｅＮａｍｅ｛Ｐａｔｔｅｒｎ｝
｛ＰａｔｔｅｒｎＶａｒｉａｂｌｅＤｅｃｌ｝
ＰａｔｔｅｒｎＶａｒｉａｂｌｅＤｅｃｌ
：：＝ＰａｔｔｅｒｎＶａｒｉａｂｌｅ Ａｇｄａ Ｔｙｐｅ
ＳｉｎｇｌｅＣｌａｕｓｅＳｉｇｎａｔｕｒｅは、定義されるところのＤ−Ｃａｓｅの名前Ｄ−ＣａｓｅＮａｍｅと、それがとり得る０個以上の引数のＰａｔｔｅｒｎと、そのＰａｔｔｅｒｎ中の各ＰａｔｔｅｒｎＶａｒｉａｂｌｅとその型の情報をもつ０個以上のＰａｔｔｅｒｎＶａｒｉａｂｌｅＤｅｃｌとから構成される。ＳｉｎｇｌｅＣｌａｕｓｅＤｅｃｌは、ＳｉｎｇｌｅＣｌａｕｓｅＳｉｇｎａｔｕｒｅと、その中の各ＰａｔｔｅｒｎＶａｒｉａｂｌｅをパラメータとして含むディーケースから構成される。これは、上述の説明における関数定義で、ＦｕｎｃｔｉｏｎＣｌａｕｓｅをひとつだけ持つＦｕｎｃｔｉｏｎＤｅｆｉｎｉｔｉｏｎに相当する。（なお、ＰａｔｔｅｒｎＶａｒｉａｂｌｅの型は、ＡｇｄａＴｙｐｅでなくともそれに変換可能なものであってもよいが、この具体例では簡単のためＡｇｄａＴｙｐｅとしている。）
【０１２３】
また、この具体例では、ディーケース宣言を議論構造情報に対応する有向非巡回グラフとして表す場合には、ディーケース宣言中のディーケースのグラフのルートノードの子ノードとして、ＳｉｎｇｌｅＣｌａｕｓｅＳｉｇｎａｔｕｒｅに含まれるＤＣａｓｅＮａｍｅ｛Ｐａｔｔｅｒｎ｝ ｛ＰａｔｔｅｒｎＶａｒｉａｂｌｅＤｅｃｌ｝の情報を有するコンテキストノードを生成するものとする。そのコンテキストノードにおいて、ＤＣａｓｅＮａｍｅ｛Ｐａｔｔｅｒｎ｝は、Ｃｌａｕｓｅとしてコンテキストに含められ、各パラメータと、その型とを示す｛ＰａｔｔｅｎＶａｒｉａｂｌｅＤｅｃｌ｝は、Ｐａｒａｍｅｔｅｒｓとしてコンテキストに含められるものとする。
【０１２４】
次に、Ａｇｄａで記述された検査対象情報において、ケースに応じた記述の特定の処理（ステップＳ２０１）について簡単に説明する。まず、この具体例では、関数ＦｕｎｃｔｉｏｎＮａｍｅの関数定義に、それがケースに応じた記述を含むという情報を付加するＰｒａｇｍａ「｛−＃ ＤＣＡＳＥ ＦｕｎｃｔｉｏｎＮａｍｅ ｒｏｏｔ ＃−｝」を導入する。翻訳部１６は、検査対象情報において、このようなＰｒａｇｍａをもつＦｕｎｃｔｉｏｎＤｅｆｉｎｉｔｉｏｎを見つける。ここでは、そのようなＦｕｎｃｔｉｏｎＤｅｆｉｎｉｔｉｏｎが、一だけＦｕｎｃｔｉｏｎＣｌａｕｓｅを持つ場合について説明する。このＦｕｎｃｔｉｏｎＣｌａｕｓｅのＲｉｇｈｔＨａｎｄＳｉｄｅであるところのＡｇｄａ項が、Ｄ−Ｃａｓｅとして特定される。これがステップＳ２０１でいうケースに応じた記述となるため、それについて図３のフローチャートにおけるステップＳ２０２以降の処理が実行されることになる。その結果として、このＤ−Ｃａｓｅに対応するディーケースのグラフ（グラフ情報）を得る。
【０１２５】
また、この具体例では、翻訳部１６は、一のそのようなＦｕｎｃｔｉｏｎＤｅｆｉｎｉｔｉｏｎ全体を、一のディーケース宣言（ＳｉｎｇｌｅＣｌａｕｓｅＤｅｃｌ）のグラフに変換するように拡張されている。具体的には、翻訳部１６は、ＬｅｆｔＨａｎｄＳｉｄｅのＦｕｎｃｔｉｏｎＮａｍｅをＳｉｎｇｌｅＣｌａｕｓｅＳｉｇｎａｔｕｒｅのＤＣａｓｅＮａｍｅとし、ＬｅｆｔＨａｎｄＳｉｄｅの｛Ｐａｔｔｅｒｎ｝をＳｉｎｇｌｅＣｌａｕｓｅＳｉｇｎａｔｕｒｅの｛Ｐａｔｔｅｒｎ｝とし、ＬｅｆｔＨａｎｄＳｉｄｅとＴｙｐｅＳｉｇｎａｔｕｒｅから、Ａｇｄａプルーフチェッカーの機能を用いて、ＳｉｎｇｌｅＣｌａｕｓｅＳｉｇｎａｔｕｒｅの｛ＰａｔｔｅｒｎＶａｒｉａｂｌｅＤｅｃｌ｝を推測して生成して、ＳｉｎｇｌｅＣｌａｕｓｅＳｉｇｎａｔｕｒｅを構成する。翻訳部１６は、これを上述の説明のようなコンテキストノードとし、ＲｉｇｈｔＨａｎｄＳｉｄｅであるところのＡｇｄａ項に対応するグラフのルートノードに子として追加する。
【０１２６】
次に、この具体例における一の特定のＤ−Ｃａｓｅに基づいて詳細を説明する。ユーザは、キーボードを操作することにより、図１０で示される検査対象情報２００を入力し、その検査対象情報２００が受付部１８で受け付けられ、検査対象記憶部１１に蓄積され、表示部１７によって表示されたとする（ステップＳ１０４〜Ｓ１０６）。図１０において、検査対象情報２００には、モデル情報２０１と、議論構造情報２０２とが含まれている。モデル情報２０１において、ＴｏｐＧｏａｌ，ＳｕｂＧｏａｌ−Ａ，ＳｕｂＧｏａｌ−Ｂは、Ｓｅｔ型を有していること、つまり、各々それ自体が型であることが宣言されている。Ａｇｄａ言語は命題を型として扱うため、この宣言は、各々をゴールとして宣言することになる。また、ｔｏｐＳｔｒａｔｅｇｙは、ＳｕｂＧｏａｌ−Ａ型のデータをもらい、ＳｕｂＧｏａｌ−Ｂ型のデータをもらい、ＴｏｐＧｏａｌ型のデータを返す関数の型を有していることが宣言されている。また、Ｅｖｉｄｅｎｃｅ−Ａは、ＳｕｂＧｏａｌ−Ａ型を有し、Ｅｖｉｄｅｎｃｅ−Ｂは、ＳｕｂＧｏａｌ−Ｂ型を有していることが宣言されている。また、議論構造情報２０２では、図１１で示される木構造のディーケースのグラフ情報がＡｇｄａによって記述されている。なお、この図１０で示される検査対象情報２００は、エラーの存在しないものである。したがって、ユーザが、検査対象情報について証明検査をする旨の指示を入力し、それに応じて検査部１２が証明検査を行ったとしても（ステップＳ１０１，Ｓ１０２）、エラーは検出されないことになる（ステップＳ１０３）。なお、例えば、議論構造情報２０２において、Ｅｖｉｄｅｎｃｅ−Ａを、Ｅｖｉｄｅｎｃｅ−Ｂに書き間違えていたとする。そのような検査対象情報２００について証明検査を行った場合には（ステップＳ１０１，Ｓ１０２）、議論構造情報２０２の「ＳｕｂＧｏａｌ−Ａ∋Ｅｖｉｄｅｎｃｅ−Ｂ」における「Ｅｖｉｄｅｎｃｅ−Ｂ」がエラーであることが検知され、そのＥｖｉｄｅｎｃｅ−Ｂの箇所がハイライト表示されることになる（ステップＳ１０３）。そのハイライト表示は，例えば、その箇所を赤字で表示することであってもよい。なお、ハイライト表示されていない文字は、赤字以外で表示されているものとする。ユーザは、そのハイライト表示された「Ｅｖｉｄｅｎｃｅ−Ｂ」を見ることによって、そこにエラーの存在することを容易に把握することができ、そのＥｖｉｄｅｎｃｅ−ＢをＥｖｉｄｅｎｃｅ−Ａに書き換えることによって、エラーを解消することができる（ステップＳ１０４〜Ｓ１０６）。
【０１２７】
次に、検査対象情報２００をグラフ情報に翻訳する処理について説明する。この具体例で用いるグラフ情報のデータ形式は、上述の説明で参照したＤ−Ｃａｓｅ Ｅｄｉｔｏｒの用いるＸＭＬ形式に準じる。図１０で示される検査対象情報２００が検査対象記憶部１１で記憶されている状態において、ユーザが、検査対象情報をグラフ情報に翻訳する旨の指示を整合性検査装置１に入力したとする。すると、その指示は受付部１８で受け付けられ、翻訳部１６に渡される。そして、翻訳部１６は、検査対象情報をグラフ情報に翻訳するタイミングであると判断し（ステップＳ１１０）、検査対象情報をグラフ情報に翻訳する処理を行う（ステップＳ１１１）。具体的には、翻訳部１６は、検査対象情報２００において、Ｐｒａｇｍａ｛−＃ ＤＣＡＳＥ ｍｙ−Ｄ−Ｃａｓｅ ｒｏｏｔ ＃−｝を特定し、関数名（ＦｕｎｃｔｉｏｎＮａｍｅ）「ｍｙ−Ｄ−Ｃａｓｅ」を取得する。また、翻訳部１６は、その関数名を用いて、ＬｅｆｔＨａｎｄＳｉｄｅである「ｍｙ−Ｄ−Ｃａｓｅ」を特定し、それと等号で関係付けられているＲｉｇｈｔＨａｎｄＳｉｄｅであるＤ−Ｃａｓｅを特定する（ステップＳ２０１）。すなわち、特定されたＤ−Ｃａｓｅは、
ＴｏｐＧｏａｌ∋
ｔｏｐＳｔｒａｔｅｇｙ
・（ＳｕｂＧｏａｌ−Ａ∋Ｅｖｉｄｅｎｃｅ−Ａ）
・（ＳｕｂＧｏａｌ−Ｂ∋Ｅｖｉｄｅｎｃｅ−Ｂ）
である。
【０１２８】
その後、翻訳部１６は、図示しない経路を介して実行部１４に対して、検査対象情報２００を実行するかどうか判断するように指示する。すると、実行部１４は、検査対象記憶部１１で記憶されている検査対象情報２００を参照し、議論構造情報２０２において、プログラムで記載されている箇所は存在しないため、実行する必要がないと判断し（ステップＳ２０２）、その結果を図示しない経路を介して翻訳部１６に渡す。
【０１２９】
その判断結果を受け取ると、翻訳部１６は、上記のＤ−Ｃａｓｅに対してケースに応じた記述の処理（ステップＳ２０４）を行う。具体的には、翻訳部１６は、パターンマッチングにより、「ｇ∋ｔ」のパターンを特定し（ステップＳ３０１）、そのパターンのｇに対応するゴールノードを生成する（ステップＳ３０２）。すなわち、翻訳部１６は、図１２Ａで示されるグラフ情報３００におけるＴｏｐＧｏａｌに対応するノードの情報３０１を生成する。ノードの情報３０１において、ｔｙｐｅ＝"Ｇｏａｌ"は、そのノードがゴールノードであることを示している。ストラテジノードの場合には、ｔｙｐｅ＝"Ｓｔｒａｔｅｇｙ"となり、エビデンスノードの場合には、ｔｙｐｅ＝"Ｅｖｉｄｅｎｃｅ"となり、コンテキストノードの場合には、ｔｙｐｅ＝"Ｃｏｎｔｅｘｔ１"となる（なお、「Ｃｏｎｔｅｘｔ」ではなく、「Ｃｏｎｔｅｘｔ１」となる理由については後述する）。ｉｄ＝"００１"は、ノードの識別子であり、ノードの生成時に、各ノードを識別できるように付与されるものである。この具体例では、各ノードの情報を生成するごとに、ｉｄが１ずつインクリメントされるものとする。ｎａｍｅ＝"Ｇ１"は、グラフ情報の表示の際に表示されるノードの名称である。このノードの名称も、ノードの生成時に適宜、生成されるものである。この具体例では、ｔｙｐｅの先頭の文字と数字とを組み合わせ、重複しないように生成される。ｖａｌｕｅ＝"ＴｏｐＧｏａｌ"は、検査対象情報２００における項の値である。なお、タグ＜ｄｃａｓｅ：ｄｅｓｃｒｉｐｔｉｏｎ＞と、タグ＜／ｄｃａｓｅ：ｄｅｓｃｒｉｐｔｉｏｎ＞との間には何も情報が含まれていないが、ゴールの項が＜＜ＦｏｒｍａｌＧｏａｌ／Ｄｅｓｃｒｉｐｔｉｏｎ＞＞のように記述されていた場合には、そのＤｅｓｃｒｉｐｔｉｏｎ（記述）が、両タグの間に含められることになる。他のノードの情報を生成する際にも、翻訳部１６は、ｔｙｐｅやｉｄ、ｎａｍｅを生成し、検査対象情報２００からＤｅｓｃｒｉｐｔｉｏｎや項の値を読み出すことによって、そのノードの情報を生成するものとする。
【０１３０】
次に、翻訳部１６は、残りがケースであるかどうか判断する。この場合には、ステップＳ３０１において、「ｇ∋ｔ」のパターンが特定されたため、残りはアーギュメントであるため、翻訳部１６は、残りはケースではないと判断して、アーギュメントに応じた記述の処理を行う（ステップＳ３０３，Ｓ３０５）。具体的には、翻訳部１６は、残りの部分である
ｔｏｐＳｔｒａｔｅｇｙ
・（ＳｕｂＧｏａｌ−Ａ∋Ｅｖｉｄｅｎｃｅ−Ａ）
・（ＳｕｂＧｏａｌ−Ｂ∋Ｅｖｉｄｅｎｃｅ−Ｂ）
について、パターンマッチングにより、「ｆ・ｔ_１・ｔ_２」のパターンを特定し（ステップＳ４０１）、ｎ＝２であるため、そのパターンのｆに対応するストラテジノードを生成する（ステップＳ４０２）。すなわち、翻訳部１６は、図１２Ａで示されるグラフ情報３００におけるｔｏｐＳｔｒａｔｅｇｙに対応するノードの情報３０２を生成する。そのノードの情報３０２の生成方法は、前述したノードの情報３０１の生成方法と同様である。その後、翻訳部１６は、ステップＳ４０１においてパターン「ｆ・ｔ_１・ｔ_２」が特定されたため、生成したノードはリーフではなく、残りはケースであると判断し（ステップＳ４０３，Ｓ４０４）、まずｔ_１である
ＳｕｂＧｏａｌ−Ａ∋Ｅｖｉｄｅｎｃｅ−Ａ
について、ケースに応じた記述の処理を行う（ステップＳ４０５）。
【０１３１】
具体的には、翻訳部１６は、パターンマッチングにより、「ｇ∋ｔ」のパターンを特定し（ステップＳ３０１）、そのパターンのｇに対応するゴールノードを生成する（ステップＳ３０２）。すなわち、翻訳部１６は、グラフ情報３００におけるＳｕｂＧｏａｌ−Ａに対応するノードの情報３０３を生成する。そして、翻訳部１６は、残りがアーギュメントであると判断し、そのアーギュメントに応じた記述の処理を行う（ステップＳ３０３，Ｓ３０４）。具体的には、翻訳部１６は、残りの部分である
Ｅｖｉｄｅｎｃｅ−Ａ
について、パターンマッチングにより、「ｆ」のパターンを特定し（ステップＳ４０１）、ｎ＝０であるため、そのパターンのｆに対応するエビデンスノードを生成する（ステップＳ４０２）。すなわち、翻訳部１６は、グラフ情報３００におけるＥｖｉｄｅｎｃｅ−Ａに対応するノードの情報３０４を生成する。その後、翻訳部１６は、エビデンスノードを生成したため、リーフであると判断し（ステップＳ４０３）、ゴールノード（ＳｕｂＧｏａｌ−Ａ）から、エビデンスノード（Ｅｖｉｄｅｎｃｅ−Ａ）へのリンクを生成する（ステップＳ３０６）。すなわち、翻訳部１６は、図１２Ｂで示されるグラフ情報３００におけるＳｕｂＧｏａｌ−ＡからＥｖｉｄｅｎｃｅ−Ａまでのリンクの情報３１１を生成する。リンクの情報３１１において、ｓｏｕｒｃｅ＝"００３"は、リンク元のノード、すなわち、ＳｕｂＧｏａｌ−Ａのノードの識別子である。また、ｔａｒｇｅｔ＝"００４"は、リンク先のノード、すなわち、Ｅｖｉｄｅｎｃｅ−Ａのノードの識別子である。ｉｄ＝"Ｌｉｎｋ−００３−００４"は、リンクの識別子であり、各リンクを識別できるように、リンクの生成時に、リンク元のノードの識別子とリンク先のノードの識別子とを用いて生成される。ｎａｍｅ＝"Ｌｉｎｋ−００３−００４"は、リンクの名称であり、この具体例では、リンクの識別子と同じである。他のリンクの情報を生成する際にも、翻訳部１６は、リンク元の識別子とリンク先の識別子とを用いて、ｓｏｕｒｃｅやｔａｒｇｅｔ、ｉｄ等を生成するものとする。
【０１３２】
その後、ｔ_１に対応するケースに応じた記述の処理が終了したため、翻訳部１６は、そのケースと、ｔｏｐＳｔｒａｇｅｇｙに対応するストラテジノードとの間のリンクを生成する（ステップＳ４０６）。すなわち、翻訳部１６は、図１２Ｂで示されるグラフ情報３００におけるｔｏｐＳｔｒａｇｅｇｙから、ｔ_１のルートであるＳｕｂＧｏａｌ−Ａまでのリンクに応じたリンクの情報３１２を生成する。
【０１３３】
その後、翻訳部１６は、未処理のケースｔ_２があるため（ステップＳ４０７）、そのｔ_２である
ＳｕｂＧｏａｌ−Ｂ∋Ｅｖｉｄｅｎｃｅ−Ｂ
について、ｔ_１の場合と同様に、ケースに応じた記述の処理を行う（ステップＳ４０５）。
【０１３４】
具体的には、翻訳部１６は、「ｇ∋ｔ」のパターンを特定し（ステップＳ３０１）、そのパターンのｇに対応するゴールノードに応じたノードの情報３０５を生成する（ステップＳ３０２）。そして、翻訳部１６は、残りがアーギュメントであると判断し、そのアーギュメントに応じた記述の処理を行う（ステップＳ３０３，Ｓ３０４）。具体的には、翻訳部１６は、残りの部分である
Ｅｖｉｄｅｎｃｅ−Ｂ
について、「ｆ」のパターンを特定し（ステップＳ４０１）、そのパターンのｆに対応するエビデンスノードに応じたノードの情報３０６を生成する（ステップＳ４０２）。その後、翻訳部１６は、エビデンスノードを生成したため、リーフであると判断し（ステップＳ４０３）、ゴールノード（ＳｕｂＧｏａｌ−Ｂ）から、エビデンスノード（Ｅｖｉｄｅｎｃｅ−Ｂ）へのリンクに応じたリンクの情報３１３を生成する（ステップＳ３０６）。そして、ｔ_２に対応するケースに応じた記述の処理が終了したため、翻訳部１６は、ｔｏｐＳｔｒａｇｅｇｙから、ｔ_２のルートであるＳｕｂＧｏａｌ−Ｂまでのリンクに応じたリンクの情報３１４を生成する（ステップＳ４０６）。
【０１３５】
これらの処理によって、ｔｏｐＳｔｒａｇｅｇｙ以下の各ノードや各リンクを生成する処理が終了したため、翻訳部１６は、ゴールノード（ＴｏｐＧｏａｌ）からアーギュメントのルートであるストラテジノード（ｔｏｐＳｔｒａｇｅｇｙ）までのリンクに応じたリンクの情報３１５を生成する（ステップＳ３０６）。
【０１３６】
その後、翻訳部１６は、検査対象情報２００にモデル情報やＤ−Ｃａｓｅの名称が存在するため、そのモデル情報２０１に応じたタグや、Ｄ−Ｃａｓｅの名称に応じたコンテキストノードを追加すると判断し（ステップＳ２０５）、ＬｅｆｔＨａｎｄＳｉｄｅに対応する「ｍｙ−Ｄ−Ｃａｓｅ」を含むコンテキストノードに応じたノードの情報３０７と、Ｄ−ＣａｓｅのルートであるＴｏｐＧｏａｌのゴールノードから、そのコンテキストノードまでのリンクに応じたリンクの情報３１６とを生成する。なお、そのコンテキストノードの情報３０７において、演算子ＣＯＮＴＥＸＴ［ ／ ］から生成されたコンテキストノードと区別するため、ｔｙｐｅ＝"ｃｏｎｔｅｘｔ２"としている。なお、演算子ＣＯＮＴＥＸＴ［ ／ ］から生成されたコンテキストノードから生成されたコンテキストノードでは、ｔｙｐｅ＝"ｃｏｎｔｅｘｔ１"になるものとする。また、そのコンテキストノードでは、そのＬｅｆｔＨａｎｄＳｉｄｅの情報（ここでは、Ｄ−Ｃａｓｅの名称）がｖａｌｕｅではなく、ｄｅｓｃｒｉｐｔｉｏｎに含められるものとする。さらに、翻訳部１６は、グラフ情報３００において、モデル情報２０１に応じたプロパティーの情報３２１を生成する（ステップＳ２０６）。このようにして、グラフ情報３００が生成されることになる。なお、プロパティーの情報３２１において、「＆＃ｘＤ；＆＃ｘＡ；」は、改行の文字コードであり、「＆＃８５９４；」は右矢印「→」の文字コードである。また、グラフ情報３００の先頭と後端のＤ−Ｃａｓｅに関するタグや、ノードやリンクの情報の前後に記載されているタグ等は、グラフ情報３００を生成するはじめの時点において生成されてもよく、あるいは、ノードやリンク、プロパティー等のタグが生成された後に生成されてもよい。その後、表示部１７は、グラフ記憶部１５で記憶されているグラフ情報３００を読み出し、各ノードの親子関係を取得して、各ノードの親子関係を示す図１１の画像を表示する（ステップＳ１１２）。図１１において、ｔｙｐｅ＝"Ｇｏａｌ"であるノード２１１，２１４，２１６は、矩形で表示され、ｔｙｐｅ＝"Ｓｔｒａｔｅｇｙ"であるノード２１３は、平行四辺形で表示され、ｔｙｐｅ＝"Ｅｖｉｄｅｎｃｅ"であるノード２１５，２１７は、楕円で表示され、ｔｙｐｅ＝"ＣｏｎｔｅｘｔＮ"（Ｎは１以上の整数）であるノード２１２は、角丸四角形で表示される。それらの図形は、図示しない記録媒体において記憶されており、表示部１７は、それらの図形を適宜、読み出すことによって、各ノードに応じた図形を表示してもよい。また、表示部１７は、その図形中に、ノードの種類（ｔｙｐｅ）と、ノードの名称（ｎａｍｅ）、ノードの値（ｖａｌｕｅ）、ノードの記述（Ｄｅｓｃｒｉｐｔｉｏｎ）に応じた文字列を生成して表示する。また、表示部１７は、グラフ情報３００に含まれる各リンクの情報に応じて、各ノードをつなぐリンクの図形（矢印の図形）２２１〜２２６をも生成して表示する。このようにして、ユーザは、検査対象情報２００に対応したグラフ情報３００を知ることができる。なお、この具体例では、モデル情報がグラフ情報においてはすべて不可視情報となっているため、グラフには表示されないことになる。
【０１３７】
なお、図１２Ａ，図１２Ｂで示される、ＸＭＬで記述されたグラフ情報３００は、実際のＤ−Ｃａｓｅ Ｅｄｉｔｏｒで用いられるＸＭＬの表記とは細部において異なっているが、実質的には同様のものである。また、グラフ情報において、ケースに含まれる各ノードの親子関係を示す方法は問わない。したがって、図１２Ａ，図１２Ｂで示される以外のデータ構造によって、グラフ情報を示してもよいことは言うまでもない。また、そのＸＭＬで記述されたグラフ情報３００を図１１で示されるように図的に表示する際に、ｄｅｓｃｒｉｐｔｉｏｎのタグで特定される文字列の表示と、図１１で示されるｖａｌｕｅの表示とを切り替えられるようにしてもよく、または、そうではなく、両方を一緒に表示するようにしてもよい。前者の場合であっても、コンテキストノードについては、ｄｅｓｃｒｉｐｔｉｏｎのタグで特定される文字列を絶えず表示するようにしてもよい。
【０１３８】
次に、グラフ情報を検査対象情報に翻訳する処理について説明する。ここでは、グラフ記憶部１５において、図１２Ａ，図１２Ｂで示されるグラフ情報３００が記憶されているものとする。なお、そのグラフ情報３００は、例えば、ユーザが、Ｄ−Ｃａｓｅ Ｅｄｉｔｏｒ等を用いて入力したものであってもよい（ステップＳ１０７〜Ｓ１０９）。そして、ユーザが、グラフ情報を検査対象情報に翻訳する旨の指示を整合性検査装置１に入力したとする。すると、その指示は受付部１８で受け付けられ、翻訳部１６に渡される。そして、翻訳部１６は、グラフ情報を検査対象情報に翻訳するタイミングであると判断し（ステップＳ１１３）、グラフ情報を検査対象情報に翻訳する処理を行う（ステップＳ１１４）。具体的には、翻訳部１６は、グラフ情報３００のリンクの情報３１１〜３１６を参照し、ｓｏｕｒｃｅには存在するがｔａｒｇｅｔには存在しないノード、すなわち、ルートノードを特定する（ステップＳ５０１）。この場合には、ｉｄ＝"００１"のノードがルートノードとなる。そのルートノードはディーケースのグラフのルートノードでもあるため、翻訳部１６は、ケースの処理を行う（ステップＳ５０２）。具体的には、ｉｄ＝"００１"である特定したルートノードがｓｏｕｒｃｅである１番目のリンクの情報３１５を特定し、そのｓｏｕｒｃｅのノードと、ｔａｒｇｅｔのノードとを特定する。この場合には、ｓｏｕｒｃｅのノードがゴールノードであり、ｔａｒｇｅｔのノードがストラテジノードとなる。したがって、翻訳部１６は、（親ノード、子ノード）＝（ゴールノード、ストラテジノード）のパターンを特定する（ステップＳ６０１，Ｓ６０２）。この場合には、リンク先がアーギュメントであるため、翻訳部１６は、アーギュメントの処理を行う（ステップＳ６０３，Ｓ６０４）。具体的には、アーギュメントのルートノード（ｉｄ＝"００２"のストラテジノード）をリンク元とするリンクの情報３１２，３１４が存在するため、翻訳部１６は、アーギュメントのルートノードにリンク先のノードが存在すると判断し（ステップＳ７０１）、そのリンクのうち、１番目のリンクの情報３１２を特定する（ステップＳ７０２，Ｓ７０３）。また、翻訳部１６は、その特定したリンクのリンク先がケースであるかどうか判断する（ステップＳ７０４）。すなわち、翻訳部１６は、特定したリンクの情報３１２からリンク先（ｔａｒｇｅｔ）のｉｄ＝"００３"を取得し、そのｉｄ＝"００３"のノードの情報３０３を特定する。そして、その特定したノードの情報３０３に含まれるノードの種類（ｔｙｐｅ）がゴールであるため、翻訳部１６は、リンク先がケースであると判断する。そして、そのリンク先のケースの処理を行う（ステップＳ７０５）。
【０１３９】
具体的には、翻訳部１６は、処理対象であるケースのルートノード（ｉｄ＝"００３"のノード）がｓｏｕｒｃｅである１番目のリンクの情報３１１を特定し、そのｓｏｕｒｃｅのノードと、ｔａｒｇｅｔのノードと関係、すなわち、（親ノード、子ノード）＝（ゴールノード、エビデンスノード）のパターンを特定する（ステップＳ６０１，Ｓ６０２）。この場合には、リンク先がアーギュメントであるため、翻訳部１６は、アーギュメントの処理を行う（ステップＳ６０３，Ｓ６０４）。具体的には、アーギュメントのルートノード（ｉｄ＝"００４"のエビデンスノード）をリンク元とするリンクの情報が存在しないため、翻訳部１６は、アーギュメントのルートノードにリンク先のノードが存在しないと判断し（ステップＳ７０１）、そのルートノードに応じた項、すなわち、
Ｅｖｉｄｅｎｃｅ−Ａ
を生成する（ステップＳ７１０）。この項は、そのルートノードのノードの情報３０４のｖａｌｕｅを用いて生成される。この場合には、その項がそのままアーギュメントの項となる（ステップＳ７１１）。その後、翻訳部１６は、そのノード（ｉｄ＝"００４"のエビデンスノード）をリンク先とするリンクの情報３１１のパターン（ゴールノード、エビデンスノード）に応じた演算子「∋」を生成する（ステップＳ６０６）。また、ｉｄ＝"００３"のゴールノードには、それ以上のリンク先が存在しないため（ステップＳ６０７，Ｓ６０８）、翻訳部１６は、そのｉｄ＝"００３"のゴールノードに応じたノードの情報３０３を用いて、そのノードに応じた項「ＳｕｂＧｏａｌ−Ａ」を生成する（ステップＳ６０９）。そして、リンク先のアーギュメントが１個であり、リンク先のアーギュメント以外の項は存在しないため（ステップＳ６１０）、翻訳部１６は、リンク先のアーギュメントの項と、ゴールノードの項とを演算子「∋」でつなぐケースの項を生成する（ステップＳ６１１）。そのケースの項は、
ＳｕｂＧｏａｌ−Ａ∋Ｅｖｉｄｅｎｃｅ−Ａ
となる。その後、翻訳部１６は、そのｉｄ＝"００３"のゴールノードをリンク先とするリンクの情報３１２のパターン（ストラテジノード、ゴールノード）に応じた演算子「・」を生成し、それを一時的に図示しない記録媒体に蓄積する（ステップＳ７０７）。また、翻訳部１６は、ｉｄ＝"００２"のストラテジノードをリンク元とする２番目のリンクの情報３１４を特定する（ステップＳ７０８，Ｓ７０９，Ｓ７０３）。また、翻訳部１６は、その特定したリンクのリンク先がｉｄ＝"００５"のゴールノードであるため、リンク先がケースであると判断する（ステップＳ７０４）。そして、そのリンク先のケースの処理を行う（ステップＳ７０５）。前述の処理と同様に、このケースの処理によって、翻訳部１６は、ｉｄ＝"００６"のエビデンスノードに対応する項と、そのエビデンスノードをリンク先とするリンクのパターンに応じた演算子「∋」と、そのリンクのリンク元であるｉｄ＝"００５"のゴールノードに対応する項と、そのゴールノードをリンク先とするリンクのパターンに応じた演算子「・」とを生成し、それを一時的に図示しない記録媒体に蓄積する（ステップＳ７０７）。その後、翻訳部１６は、ｉｄ＝"００２"のストラテジノードに応じた項を生成する（ステップＳ７１０）。リンク先は、ケースの項が２個のみであるため、翻訳部１６は、リンク先の２個のケースの項と、ストラテジノードの項とを演算子「・」でそれぞれつなぐアーギュメントの項を生成する（ステップＳ７１１）。そのアーギュメントの項は、
ｔｏｐＳｔｒａｇｅｇｙ
・（ＳｕｂＧｏａｌ−Ａ∋Ｅｖｉｄｅｎｃｅ−Ａ）
・（ＳｕｂＧｏａｌ−Ｂ∋Ｅｖｉｄｅｎｃｅ−Ｂ）
となる。そして、ｉｄ＝"００２"のストラテジノードをルートノードとするアーギュメントの処理が終了したため、翻訳部１６は、そのストラテジノードがリンク先であるリンクの情報３１５に応じた演算子「∋」を生成し（ステップＳ６０６）、さらに、全体のケースのルートノードであるｉｄ＝"００１"のゴールノードに応じた項「ＴｏｐＧｏａｌ」を生成する（ステップＳ６０７〜Ｓ６０９）。そして、リンク先のアーギュメントが１個であり、リンク先のアーギュメント以外の項は存在しないため（ステップＳ６１０）、翻訳部１６は、リンク先のアーギュメントの項と、ゴールノードの項とを演算子「∋」でつなぐケースの項を生成する（ステップＳ６１１）。そのケースの項は、
ＴｏｐＧｏａｌ∋
ｔｏｐＳｔｒａｇｅｇｙ
・（ＳｕｂＧｏａｌ−Ａ∋Ｅｖｉｄｅｎｃｅ−Ａ）
・（ＳｕｂＧｏａｌ−Ｂ∋Ｅｖｉｄｅｎｃｅ−Ｂ）
となる。なお、グラフ情報３００には、コンテキストノードに対応したノードの情報３０７と、それに応じたリンクの情報３１６とが存在するが、そのコンテキストの種類（ｔｙｐｅ）は、「Ｃｏｎｔｅｘｔ２」であるため、翻訳部１６は、通常の演算子ＣＯＮＴＥＮＴ「 ／ 」を生成する処理を行わない。そして、そのｔｙｐｅ＝"Ｃｏｎｔｅｘｔ２"のノードの情報３０７と、プロパティーの情報３２１とが存在するため、翻訳部１６は、検査対象情報に追加する情報が存在すると判断し（ステップＳ５０３）、ｔｙｐｅ＝"Ｃｏｎｔｅｘｔ２"のノードの情報３０７のｄｅｓｃｒｉｐｔｉｏｎ「ｍｙ−Ｄ−Ｃａｓｅ」が左辺となり、その左辺と、すでに生成された上述のＤ−Ｃａｓｅの記述とを等号でつなぐ。また、プロパティーの情報３２１からモデル情報を読み出し、検査対象情報に追加する（ステップＳ５０４）。その結果、最終的な検査対象情報は、次のようになる。このようにして、グラフ情報から検査対象情報への翻訳が行われる。
【０１４０】
ｐｏｓｔｕｌａｔｅ
ＴｏｐＧｏａｌ ＳｕｂＧｏａｌ−Ａ ＳｕｂＧｏａｌ−Ｂ：Ｓｅｔ
ｔｏｐＳｔｒａｔｅｇｙ：ＳｕｂＧｏａｌ−Ａ→ＳｕｂＧｏａｌ−Ｂ→ＴｏｐＧｏａｌ
Ｅｖｉｄｅｎｃｅ−Ａ：ＳｕｂＧｏａｌ−Ａ
Ｅｖｉｄｅｎｃｅ−Ｂ：ＳｕｂＧｏａｌ−Ｂ
ｍｙ−Ｄ−Ｃａｓｅ＝
ＴｏｐＧｏａｌ∋
ｔｏｐＳｔｒａｇｅｇｙ
・（ＳｕｂＧｏａｌ−Ａ∋Ｅｖｉｄｅｎｃｅ−Ａ）
・（ＳｕｂＧｏａｌ−Ｂ∋Ｅｖｉｄｅｎｃｅ−Ｂ）
【０１４１】
この検査対象情報は、表示部１７によって表示され（ステップＳ１１５）、ユーザは、その検査対象情報について適宜、追記や変更を行うことができる。また、検査を行うことによって、不適切な箇所を検出することもできる（ステップＳ１０１〜Ｓ１０３）。
【０１４２】
ここで、翻訳部１６は、検査対象情報をグラフ情報に翻訳することができ、また、グラフ情報を検査対象情報に翻訳することができる。したがって、翻訳部１６は、検査対象情報をグラフ情報に翻訳し、その後に、そのグラフ情報を検査対象情報に翻訳することもできる。その際に、翻訳前の検査対象情報と、グラフ情報から翻訳された検査対象情報とは、同じであってもよく、あるいは、異なってもよい。例えば、後述するように、検査対象情報をグラフ情報に翻訳する際に、実行部１４による実行が行われた場合には、通常、両検査対象情報は異なるものとなる。
【０１４３】
［検査対象情報の実行］
上述の具体例では、検査対象情報をグラフ情報に翻訳する際に、実行部１４による実行が不要である場合について説明したが、前述のように、実行部１４による実行を行った上で翻訳を行ってもよい。その場合には、例えば、検査対象記憶部１１において、図１３で示される検査対象情報が記憶されていたとする。この場合には、Ｄ−Ｃａｓｅに応じた記述は、
ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ Ｇ ｓｔｅｐ ｂａｓｅ ３
であるが、これは、その記載の上側で定義されている生成関数（プログラム）「ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ」と、四の引数「Ｇ」、「ｓｔｅｐ」、「ｂａｓｅ」、「３」とによって記述されたものである。したがって、この図１３の検査対象情報をグラフ情報に翻訳する際には、翻訳部１６によってケースに応じた上記記述が特定され（ステップＳ２０１）、実行部１４によって実行が必要であると判断されて（ステップＳ２０２）、その生成関数（プログラム）が実行されることになる（ステップＳ２０３）。
【０１４４】
具体的には、引数の具体的な値が「Ｇ」、「ｓｔｅｐ」、「ｂａｓｅ」、「３」であるため、生成関数（プログラム）「ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ」を繰り返して適用することにより、次のようになる。
ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ Ｇ ｓｔｅｐ ｂａｓｅ ３
＝Ｇ ３∋ｓｔｅｐ ２
・ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ Ｇ ｓｔｅｐ ｂａｓｅ ２
＝Ｇ ３∋ｓｔｅｐ ２
・（Ｇ ２∋ｓｔｅｐ １
・ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ Ｇ ｓｔｅｐ ｂａｓｅ １）
＝Ｇ ３∋ｓｔｅｐ ２
・（Ｇ ２∋ｓｔｅｐ １
・（Ｇ １∋ｓｔｅｐ ０
・ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ Ｇ ｓｔｅｐ ｂａｓｅ ０））
＝Ｇ ３∋ｓｔｅｐ ２
・（Ｇ ２∋ｓｔｅｐ １
・（Ｇ １∋ｓｔｅｐ ０
・（Ｇ ０∋ｂａｓｅ）））
【０１４５】
したがって、最終的に、図１０の検査対象情報２００と同様に、項と演算子とを陽に記述する形式の検査対象情報（議論構造情報）を得ることができ、翻訳部１６は、その検査対象情報を、図１４のように表示されるグラフ情報に翻訳することができる。なお、ここでは、翻訳の前にすべての項と演算子とを陽に記述する形式の議論構造情報を生成してから翻訳を行う場合について説明したが、前述のように、翻訳の処理を行いながら、逐次的に実行を行ってもよいことは言うまでもない。例えば、「ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ Ｇ ｓｔｅｐ ｂａｓｅ ２」を翻訳する際に、それを実行して「Ｇ２∋ｓｔｅｐ１・ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ Ｇ ｓｔｅｐ ｂａｓｅ １」を得るようにし、さらに、「ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ Ｇ ｓｔｅｐ ｂａｓｅ １」を翻訳する際に、それを実行して「Ｇ１∋ｓｔｅｐ０・ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ Ｇ ｓｔｅｐ ｂａｓｅ ０」を得るようにしてもよい。以上のように、実行部１４によって、項と演算子とを陽に記述する形式の議論構造情報を生成してから、あるいは、生成しながら翻訳を行うことによって、引数の具体値を変更するだけで、最新のケースや、図的に表示したいケースに応じたグラフ情報を生成することができるメリットがある。例えば、上述の例の場合、検査対象情報における「Ｇ ｓｔｅｐ ｂａｓｅ ３」を適宜、「Ｇ ｓｔｅｐ ｂａｓｅ ２」や「Ｇ ｓｔｅｐ ｂａｓｅ ５」などに変更し、その後に翻訳の処理を開始することによって、ユーザは、その変更後のケースに応じた有向非巡回グラフを見ることができるようになる。
【０１４６】
なお、上述のように、項と演算子とを陽に記述する形式の議論構造情報を生成する生成関数と引数の具体値とを用いて項と演算子とを陽に記述する形式の議論構造情報を生成する場合であっても、証明検査は、生成関数と引数の具体値とを用いた記述に対して実行すればよい。その証明検査においてエラーがなければ、生成関数を実行した結果に応じた適切なグラフ情報を得られることは保証されることになる。
【０１４７】
ここで、生成関数と引数の具体値とを有する検査対象情報（議論構造情報）を一般的に記述すれば、次のようになる。なお、前述の例との対応で言えば、「ｉｎｄｕｃｔｉｏｎ−ｏｎ−Ｎ」が「ｇｅｎｅｒａｔｏｒ」に対応し、「Ｇ」、「ｓｔｅｐ」、「ｂａｓｅ」、「３」が「ｖ_１」，…，「ｖ_ｎ」に対応する。また、「ｇｅｎｅｒａｔｏｒ」の型は、
（ｘ_１：ＰａｒａｍｅｔｅｒＴｙｐｅ_１）→
（ｘ_２：ＰａｒａｍｅｔｅｒＴｙｐｅ_２）→
…
（ｘ_ｎ：ＰａｒａｍｅｔｅｒＴｙｐｅ_ｎ）→
Ｇ ｘ_１ ｘ_２ … ｘ_ｎ
すなわち、パラメータの値がｖ_１，…，ｖ_ｎのときに「ｇｅｎｅｒａｔｏｒ ｖ_１ … ｖ_ｎ」を計算すると、ｖ_１，…，ｖ_ｎに応じたゴール「Ｇ ｖ_１ … ｖ_ｎ」のケースに応じた議論構造情報（項や演算子を陽に記述したものである）が生成されることになる。
ｍｙＬａｔｅｓｔＤＣａｓｅ：Ｇ ｖ_１ … ｖ_ｎ
ｍｙＬａｔｅｓｔＤＣａｓｅ＝ｇｅｎｅｒａｔｏｒ ｖ_１ … ｖ_ｎ
｛−＃ ＤＣＡＳＥ ｍｙＬａｔｅｓｔＤＣａｓｅ ｒｏｏｔ ＃−｝
【０１４８】
［実行の拡張１］
次に、実行部１４は、項や演算子を陽に記述した議論構造情報の計算を実行することに加えて、同時に通常の計算を実行することができてもよいこと、及び、そのメリットを説明する。Ａｇｄａでは、型Ｄと、Ｄ型の引数をとる述語Ｇ（つまり「Ｇ：Ｄ→Ｓｅｔ」である）から、「Ｄ型の値ｄと、Ｇ ｄの証明（Ｄ−Ｃａｓｅに対応する議論構造）ｐのペア」の集合を値とする型Σ Ｄ Ｇを構成することができる。ここで、関数「ｏｕｔｐｕｔ−ａｎｄ−ＤＣａｓｅ：（ｘ：ＰａｒａｍｅｔｅｒＴｙｐｅ）→Σ Ｄ Ｇ」が定義されたとする（簡単のため、引数は一とする）。この関数はｘの値からＤ型の値を計算すると同時に、その計算された値がＧを満たすことの証明を返す関数となる。そこで、議論構造情報を次のようにすることによって、パラメータの値ｖに応じた何らかの結果「ｍｙＬａｔｅｓｔＯｕｔｐｕｔ」が計算され、それと同時に、その結果が述語Ｇを満たすことを示す「ｍｙＬａｔｅｓｔＤＣａｓｅ」である議論構造情報（項や演算子を陽に記述したものである）が生成されることになる。また、翻訳部１６によって、その議論構造情報をグラフ情報に翻訳することもでき、その場合には、その議論構造情報を図的に表示することも可能となる。
ｍｙＬａｔｅｓｔ：Σ Ｄ Ｇ
ｍｙＬａｔｅｓｔ＝ｏｕｔｐｕｔ−ａｎｄ−Ｄｃａｓｅ ｖ

ｍｙＬａｔｅｓｔＯｕｔｐｕｔ：Ｄ
ｍｙＬａｔｅｓｔＯｕｔｐｕｔ＝ｆｉｒｓｔ−ｃｏｍｐｏｎｅｎｔ ｍｙＬａｔｅｓｔ

ｍｙＬａｔｅｓｔＤＣａｓｅ：Ｇ ｍｙＬａｔｅｓｔＯｕｔｐｕｔ
ｍｙＬａｔｅｓｔＤＣａｓｅ＝ｓｅｃｏｎｄ−ｃｏｍｐｏｎｅｎｔ ｍｙＬａｔｅｓｔ
｛−＃ ＤＣＡＳＥ ｍｙＬａｔｅｓｔＤＣａｓｅ ｒｏｏｔ ＃−｝
【０１４９】
この場合には、議論構造情報を実行部１４が実行することにより、何らかの計算結果の値（ｍｙＬａｔｅｓｔＯｕｔｐｕｔ）と、その値が正しいことを示す議論構造（ｍｙＬａｔｅｓｔＤＣａｓｅ）とが生成されることになる。したがって、前述のように、項や演算子を陽に記述した議論構造情報を生成する場合と比較して、値が計算されていること、また、その生成された、項や演算子を陽に記述した議論構造情報が、その計算された値に関する証明となっていることが追加されていることになる。また、この場合には、値を計算するプログラムと証明（議論構造情報の陽な記述を生成するプログラム）とが一体になっているため、「このＤ−Ｃａｓｅは本当にこの値を計算するのに使ったプログラムに基づいているのか？」という心配をする必要がなくなるというメリットがある。
【０１５０】
［実行の拡張２］
上記をさらに拡張して、計算された値が、パラメータの具体的値との関係において正しいことを示すＤ−Ｃａｓｅを生成することもできる。この場合には、計算結果の型Ｄと述語Ｇとがパラメータの値に依存し、
Ｄ：ＰａｒａｍｅｔｅｒＴｙｐｅ→Ｓｅｔ
（パラメータの値に応じて結果の型も変わりうることを示す）
Ｇ：（ｘ：ＰａｒａｍｅｔｅｒＴｙｐｅ）→Ｄ ｘ→Ｓｅｔ
（パラメータの値と、結果型の値の二つを引数にとる述語、すなわち計算の入力値と出力値の間の関係、すなわち（それが成り立っていることをＤ−Ｃａｓｅで示すべきところの）計算の仕様を示す）
となる。
【０１５１】
そして、
ｏｕｔｐｕｔ−ａｎｄ−ＤＣａｓｅ：（ｘ：ＰａｒａｍｅｔｅｒＴｙｐｅ）→Σ（Ｄ ｘ）（Ｇ ｘ）
という型付けのものが定義されたとして、次のように議論構造情報を記述することによって、結果の型Ｄと述語Ｇとがパラメータｘに依存する場合に拡張することができる。
ｍｙＬａｔｅｓｔ：Σ （Ｄ ｖ） （Ｇ ｖ）
ｍｙＬａｔｅｓｔ＝ｏｕｔｐｕｔ−ａｎｄ−Ｄｃａｓｅ ｖ

ｍｙＬａｔｅｓｔＯｕｔｐｕｔ：Ｄ ｖ
ｍｙＬａｔｅｓｔＯｕｔｐｕｔ＝ｆｉｒｓｔ−ｃｏｍｐｏｎｅｎｔ ｍｙＬａｔｅｓｔ

ｍｙＬａｔｅｓｔＤＣａｓｅ：Ｇ ｖ ｍｙＬａｔｅｓｔＯｕｔｐｕｔ
ｍｙＬａｔｅｓｔＤＣａｓｅ＝ｓｅｃｏｎｄ−ｃｏｍｐｏｎｅｎｔ ｍｙＬａｔｅｓｔ
｛−＃ ＤＣＡＳＥ ｍｙＬａｔｅｓｔＤＣａｓｅ ｒｏｏｔ ＃−｝
【０１５２】
この場合には、議論構造情報を実行部１４が実行することにより、パラメータの具体的値ｖに応じた型を有する何らかの値（ｍｙＬａｔｅｓｔＯｕｔｐｕｔ）と、その値が正しいことを示す、その値とｖとに応じたトップゴール（Ｇ ｖ ｍｙＬａｔｅｓｔＯｕｔｐｕｔ）を持つ議論構造（ｍｙＬａｔｅｓｔＤＣａｓｅ）とが生成されることになる。したがって、ｍｙＬａｔｅｓｔＯｕｔｐｕｔが、最新のパラメータｖとの関係において正しいことを示す最新の議論構造が得られることになる。
【０１５３】
ここで、「検査対象情報の実行」、「実行の拡張１」、及び、「実行の拡張２」で説明した実行の対象となる議論構造情報を情報Ａと呼ぶ。上記では、いかなる過程でパラメータの具体的値ｖを含む情報Ａが検査対象記憶部１１に記憶された状態に至ってもよい。情報Ａの実行の契機となる、情報Ａを含む検査対象情報をグラフ情報に翻訳するタイミングは、上述した通り、翻訳部１６のステップＳ１１０での判断による。
【０１５４】
［実行の拡張３］
パラメータの具体的値ｖを含む情報Ａの生成と、それのグラフ情報への翻訳（情報Ａの実行を含む）は、整合性検査装置１内において、機械的に制御されていてもよい。この制御の記述（プログラム）を情報Ｂと呼ぶ。情報Ｂは、情報Ａのうちパラメータの具体的値以外の部分をそのまま含んでいてもよい。情報Ｂは、検査対象記憶部１１に記憶され、実行部１４によって実行されると、外部からの入力を取得し（例えばその時点でのセンサー読み取り値）、入力に基づいてパラメータの具体的値ｖを含む情報Ａを検査対象記憶部１１上に生成し、その情報Ａに関する計算を前段までのように実行して、その計算結果である、項や演算子が陽に記述された議論構造情報をグラフ情報に翻訳する処理を行うプログラムである。また、情報Ｂの実行は、生成された情報Ａのその他の計算結果を外部に出力してもよい（例えば、前記ｍｙＬａｔｅｓｔＯｕｔｐｕｔでアクチュエータを制御するなど）し、入力取得から翻訳・出力までの処理を繰り返してもよい。このように、情報Ｂが実行されることによって翻訳が行われる場合には、検査対象記憶部１１において、検査対象情報をグラフ情報に変換する処理に応じた変換プログラムも記憶されており、翻訳部１６は、その変換プログラムを実行することによって、検査対象情報をグラフ情報に変換すると考えてもよい。さらに、検査対象記憶部１１において、実行部１４による実行を行うためのプログラムも記憶されており、実行部１４は、そのプログラムを実行することによって、検査対象情報を実行すると考えてもよい。あるいは、翻訳部１６が実行部１４の機能を用いることができることに加えて、実行部１４が翻訳部１６の機能を呼び出したり、実行部１４が自分自身の機能を呼び出したりすることが、再帰的に可能な構成になっていると考えてもよい。なお、この実行の拡張３の場合において、情報Ｂにおける情報Ａ以外の部分は、情報Ａと同じ構成的型理論に基づく同じ人工言語で記述されていてもよく、あるいは、そうでなくてもよい。すなわち、検査対象情報と変換プログラムとは、構成的型理論に基づく同じ人工言語で記述されていてもよく、あるいは、そうでなくてもよい。また、検査対象情報と、実行部１４が実行を行うためのプログラムとは、構成的型理論に基づく同じ人工言語で記述されていてもよく、あるいは、そうでなくてもよい。
【０１５５】
［実行の拡張４］
また、前述したように、実行部１４は、証明検査において、検査対象情報に含まれるプログラム、または、検査対象情報で指定される外部プログラムを実行し、その実行結果が証明検査に用いられてもよい。その場合には、例えば、炉に関するアシュランス・ケースに応じた検査対象情報の証明検査を行う際に、外部プログラムを実行することによって、実際の炉の温度を取得し、その取得した炉の温度を用いて、証明検査を行うこともできる。また例えば、システムに関するアシュランス・ケースに応じた検査対象情報の証明検査を行う際に、そのシステムの設計情報や運用実績データ等を収めたデータベースに対するクエリーを外部プログラムとして実行して、その結果に基づいて証明検査をおこなうこともできる。また例えば、あるゴールＧのエビデンスＥとして「自動証明プログラムＰによる」という記述を許し、証明検査の際に外部プログラムＰをＧに対して実行し、その結果いかんによって元の議論構造情報Ｇ∋Ｅの検査結果を定めることもできる。また、そのような実行を行う場合には、検査対象情報が実行対象となるプログラムを含んでいてもよく、あるいは、外部プログラムが呼び出されるようにしてもよい。なお、Ａｇｄａにおいては、そのような外部プログラムを呼び出す機能（プラグイン機構）を用いた証明検査を行うことができる。そのことについては、次の文献を参照されたい。
【０１５６】
文献：Ｙｏｓｈｉｆｕｍｉ Ｙｕａｓａ，Ｙｏｓｈｉｎｏｒｉ Ｔａｎａｂｅ，Ｔｏｓｈｉｆｕｓａ Ｓｅｋｉｚａｗａ，Ｋｏｉｃｈｉ Ｔａｋａｈａｓｈｉ、「Ｖｅｒｉｆｉｃａｔｉｏｎ ｏｆ ｔｈｅ Ｄｅｕｔｓｃｈ−Ｓｃｈｏｒｒ−Ｗａｉｔｅ Ｍａｒｋｉｎｇ Ａｌｇｏｒｉｔｈｍ ｗｉｔｈ Ｍｏｄａｌ Ｌｏｇｉｃ」、Ｓｅｃｏｎｄ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ，Ｖｅｒｉｆｉｅｄ Ｓｏｆｔｗａｒｅ：Ｔｈｅｏｒｉｅｓ，Ｔｏｏｌｓ，Ｅｘｐｅｒｉｍｅｎｔｓ（ＶＳＴＴＥ ２００８），ＬＮＣＳ ５２９５，ｐ．１１５−１２９，２００８年
【０１５７】
次に、コンテキストにパラメータの情報（Ｐａｒａｍｅｔｅｒｓ）も含まれる場合の具体例について簡単に説明する。検査対象情報が図１５で示されるものであったとする。この場合には、ＤＣａｓｅＮａｍｅ｛Ｐａｔｔｅｒｎ｝ ｛ＰａｔｔｅｒｎＶａｒｉａｂｌｅＤｅｃｌ｝は、等号の左辺である「ｅｘａｍｐｌｅ−ｗｉｔｈ−ｐａｒａｍｓ Ｘ ｅ１ ｅ２」となる。そして、各パラメータは、Ｘ、ｅ１、ｅ２である。翻訳部１６は、その各パラメータの型付けが、「Ｘ：Ｓｙｓｔｅｍ」、「ｅ１：Ｘ ｉｓ−ｄｅｓｉｇｎｅｄ−ｄｅｐｅｎｄａｂｌｅ」、「ｅ２：Ｘ ｉｓ−ｄｅｖｅｌｏｐｅｄ−ｃｏｒｒｅｃｔｌｙ」であることを、ＴｙｐｅＳｉｇｎａｔｕｒｅである部分（等号より上の３行）で示されたｅｘａｍｐｌｅ−ｗｉｔｈ−ｐａｒａｍｓの型から判断する。これは、Ａｇｄａのような構成的型理論の実装において一般的な技術である型推論を行うことによってなされる。したがって、ステップＳ２０６の処理において、
Ｃｌａｕｓｅ
ｅｘａｍｐｌｅ−ｗｉｔｈ−ｐａｒａｍｓ Ｘ ｅ１ ｅ２
Ｐａｒａｍｅｔｅｒｓ
（Ｘ：Ｓｙｓｔｅｍ）
（ｅ１：Ｘ ｉｓ−ｄｅｓｉｇｎｅｄ−ｄｅｐｅｎｄａｂｌｅ）
（ｅ２：Ｘ ｉｓ−ｄｅｖｅｌｏｐｅｄ−ｃｏｒｒｅｃｔｌｙ）
を含むコンテキストノードが生成されることになる。なお、前述のように、グラフ情報において、このコンテキストノードに対応するノードの情報のｔｙｐｅは、「Ｃｏｎｔｅｘｔ２」である。また、図１５で示される検査対象情報が翻訳されたグラフ情報の表示は、図１６で示されるようになる。その図１６において、ルートノードの子ノードであるコンテキストノードにおいて、上述のＣｌａｕｓｅと、Ｐａｒａｍｅｔｅｒｓとが含まれている。
【０１５８】
また、上述の具体例では、グラフ情報３００において、モデル情報２０１をプロパティーの情報３２１に含める場合について説明したが、そうでなくてもよい。モデル情報２０１に対応したコンテキストノードを生成するようにしてもよい。そのコンテキストノードも、議論構造情報におけるルートノードの子ノードとして生成されることが好適である。また、そのコンテキストノードに含まれる記述が、グラフ情報から検査対象情報への翻訳の際にモデル情報に変換されるように、そのモデル情報を含むコンテキストノードが他のコンテキストノードと区別可能になっていることが好適である。具体的には、そのコンテキストノードに対応するノードの情報において、ｔｙｐｅを「Ｃｏｎｔｅｘｔ３」とすることによって、その区別が行われるようにしてもよい。
【０１５９】
また、検査対象情報において、ｌｅｔ構文を用いてもよい。ｌｅｔ構文を用いることによって、議論構造情報における局所的な宣言を行うことができる。例えば、前述のＤ−ＣａｓｅやＡｒｇｕｍｅｎｔを、次のように拡張してもよい。
Ｄ−Ｃａｓｅ：：＝…
｜ｌｅｔ
ＦｏｒｍａｌＣｏｎｔｅｘｔ
［ＣｏｎｔｅｘｔＤｅｓｃｒｉｐｔｉｏｎ］
ｉｎ
Ｄ−Ｃａｓｅ
Ａｒｇｕｍｅｎｔ：：＝…
｜ｌｅｔ
ＦｏｒｍａｌＣｏｎｔｅｘｔ
［ＣｏｎｔｅｘｔＤｅｓｃｒｉｐｔｉｏｎ］
ｉｎ
Ａｒｇｕｍｅｎｔ
【０１６０】
なお、…は、前述のＤ−ＣａｓｅやＡｒｇｕｍｅｎｔの記述を示すものである。具体的には、例えば、議論構造情報２０２を、次のようにｌｅｔ構文を用いて記述することも可能である。
ｍｙ−Ｄ−Ｃａｓｅ＝ｌｅｔ
Ｔ１＝ＴｏｐＧｏａｌ
Ｔ２＝ｔｏｐＳｔｒａｔｅｇｙ
Ｓ１＝ＳｕｂＧｏａｌ−Ａ
Ｓ２＝ＳｕｂＧｏａｌ−Ｂ
Ｅ１＝Ｅｖｉｄｅｎｃｅ−Ａ
Ｅ２＝Ｅｖｉｄｅｎｃｅ−Ｂ
ｉｎ
Ｔ１∋Ｔ２・（Ｓ１∋Ｅ１）・（Ｓ２∋Ｅ２）
【０１６１】
上記の例では、ｌｅｔとｉｎとの間において、ＴｏｐＧｏａｌやｔｏｐＳｔｒａｇｅｇｙ等を、Ｔ１やＴ２で記述することを宣言し、ｉｎ以下のＤ−Ｃａｓｅにおいて、項をＴ１やＴ２で記述している。なお、ｌｅｔ構文を用いて局所モデル情報を記述してもよい。すなわち、ｌｅｔとｉｎとの間に、局所モデル情報を含めるようにしてもよい。なお、検査対象情報をグラフ情報に翻訳する際に、このｌｅｔとｉｎとの間の記述は、ｉｎ以下のＤ−ＣａｓｅやＡｒｇｕｍｅｎｔにおけるルートノードの子ノードであるコンテキストノードに含めるようにしてもよい。その際にも、そのコンテキストノードに含まれる記述が、グラフ情報から検査対象情報への翻訳の際にｌｅｔ構文に変換されるように、そのｌｅｔ構文の記述を含むコンテキストノードが他のコンテキストノードと区別可能になっていることが好適である。具体的には、そのコンテキストノードに対応するノードの情報において、ｔｙｐｅを「Ｃｏｎｔｅｘｔ４」とすることによって、その区別が行われるようにしてもよい。
【０１６２】
また、検査対象情報がモジュール構造を有する例について簡単に説明する。図１７Ａ，図１７Ｂで示される検査対象情報（厳密には、検査対象情報の議論構造情報である）におけるｌｅｔ構文のｌｅｔとｉｎとの間に、「ｏｐｅｎ Ｃ−ＤｅｆＳｙｓ」や「ｏｐｅｎ Ｃ−ＳｙｓｔｅｍＳａｆｅ」が含まれている。そのことは、ｉｎ以下において、モジュール「Ｃ−ＤｅｆＳｙｓ」や「Ｃ−ＳｙｓｔｅｍＳａｆｅ」の中で記述された情報が、「ｉｎ」に続く項の中で参照されることの宣言を意味している。なお、この例でのモジュールは、モデル情報についてのものであるが、モジュール内で記述される情報はそれに限定されないことは言うまでもない。すなわち、モジュールは、モデル情報について使用されてもよく、議論構造情報について使用されてもよい。このように、検査対象情報においてモジュールが使用される範囲は問わない。検査対象情報の記述にモジュール構造を利用することによって、ソフトウェア記述におけるモジュール構造の利点を、検査対象情報の記述に導入することができるようになる。例えば、関連する情報を一箇所にまとめることにより保守性が向上する点、パラメータ付きモジュールを定義することにより汎用性が向上する点、モジュール間のインターフェースを定めた上で各モジュールを構築することにより作業を確実に分割し、また作業結果を機械的に合成することできる点、などが挙げられる。
【０１６３】
また、アーギュメントは、上述の説明以外のパターンをも有してもよい。例えば、アーギュメントは、次のように、∀Ｉｎｔｒｏや、→Ｉｎｔｒｏなどの演算子を用いて構成されてもよい。
Ａｒｇｕｍｅｎｔ：：＝…
｜∀Ｉｎｔｒｏ｛Ｄｏｍａｉｎ｝（Ｌａｍｂｄａ−Ｄ−Ｃａｓｅ）
｜→Ｉｎｔｒｏ｛Ｄｏｍａｉｎ｝（Ｌａｍｂｄａ−Ｄ−Ｃａｓｅ）
Ｌａｍｂｄａ−Ｄ−Ｃａｓｅ：：＝λ（Ａｇｄａの変数名）→Ｄ−Ｃａｓｅ
Ｄｏｍａｉｎ：：＝Ｓｅｔ型のＡｇｄａ項
なお、…は、前述のＡｒｇｕｍｅｎｔの記述を示すものである。また、「ｅ（ｘ）」が変数「ｘ」を含むＡｇｄａ項であるとき、λ表記「λ ｘ→ｅ（ｘ）」は、具体的値「ｖ」を受け取ると「ｅ（ｖ）」（ｘにｖを代入したときのｅ（ｘ）の値）を返す関数を表すＡｇｄａ項である。
【０１６４】
演算子「∀Ｉｎｔｒｏ」は、「∀（ｘ：Ｄ）→Ｐ（ｘ）」すなわち「全てのＤ型の値ｘについて、Ｐ（ｘ）が成り立つ」（ＰはＤ型の値を引数とする述語）の形のゴールを示すアーギュメントの記述を構成するために用いる。構成的型理論において、この形の命題の一の証明を与えるということは、Ｄ型の任意の値ｘを受け取って、Ｐ（ｘ）の証明を返すような一の関数を与えることである。演算子∀Ｉｎｔｒｏは、第一引数として一の型Ｄ、第二引数として一のそのような関数のλ表記「λ ｘ→（Ｐ（ｘ）∋Ａｒｇｕｍｅｎｔ（ｘ））」とをとり、ゴール「∀（ｘ：Ｄ）→Ｐ（ｘ）」を示すアーギュメントのＡｇｄａ表記「∀Ｉｎｔｒｏ｛Ｄ｝（λ ｘ→（Ｐ（ｘ）∋Ａｒｇｕｍｅｎｔ（ｘ））」を構成する。これのＡｇｄａ項としての意味は、第二引数である関数自体と同じである。アーギュメントとしては、「ｘを任意のＤ型の値を表す変数として導入し、ゴールＰ（ｘ）をアーギュメントＡｒｇｕｍｅｎｔ（ｘ）で示す」というアーギュメントである。
【０１６５】
同様に、演算子「→Ｉｎｔｒｏ」は、「Ｇ_１→Ｇ_２」すなわち「Ｇ_１ならばＧ_２」（Ｇ_１とＧ_２はゴール）の形のゴールを示すアーギュメントの記述を構成するために用いる。構成的型理論において、この形の命題の一の証明を与えるということは、Ｇ_１の任意の証明ｈを受け取って、Ｇ_２の証明を返すような一の関数を与えることである。演算子→Ｉｎｔｒｏは、第一引数として一のゴールＧ_１と、第二引数として一のそのような関数のλ表記「λ ｈ→（Ｇ_２∋Ａｒｇｕｍｅｎｔ（ｈ））」とをとり、ゴール「Ｇ_１→Ｇ_２」を示すアーギュメントのＡｇｄａ表記「→Ｉｎｔｒｏ｛Ｇ_１｝（λ ｈ→（Ｇ_２∋Ａｒｇｕｍｅｎｔ（ｈ））」を構成する。これのＡｇｄａ項としての意味は、第二引数である関数自体と同じである。アーギュメントとしては、「仮にＧ_１のエビデンスが与えられたとしてこれをｈとし、Ｇ_２をアーギュメントＡｒｇｕｍｅｎｔ（ｈ）で示す」というアーギュメントである。アーギュメントＡｒｇｕｍｅｎｔ（ｈ）の中では、Ｇ_１を示すエビデンスとしてｈを用いることができることになる。
【０１６６】
それら∀Ｉｎｔｒｏや→Ｉｎｔｒｏの両方を用いた簡単な検査対象情報の例は、図１８で示すものである。厳密には、図１８は、議論構造情報のみを示している。図１８の議論構造情報は、簡単に言えば、すべての自然数ｎについて、Ｐｎ→Ｐｎを証明するため、任意の自然数ｎについて、Ｐｎ→Ｐｎを証明するものである。そして、その任意の自然数ｎについてＰｎ→Ｐｎを証明するため、Ｐｎの証明ｐを仮定し、その証明ｐを用いることによってＰｎの成立を証明するものである。図１８で示される議論構造情報を翻訳する際には、図５のフローチャートのステップＳ４０１において、翻訳部１６は、「∀Ｉｎｔｒｏ｛Ｄ｝（λ ｘ→ｔ）」や「→Ｉｎｔｒｏ｛Ｇ_１｝（λ ｈ→ｔ）」を、ストラテジと残りのケースのパターンの一種として特定する。両者において、残りのケースは「ｔ」の部分であり、それ以外の部分の情報はストラテジノードとそのストラテジノードの子となるコンテキストノードの情報に翻訳される。具体的には、ステップＳ４０１において「∀Ｉｎｔｒｏ｛Ｄ｝（λ ｘ→ｔ）」のパターンが特定された場合には、翻訳部１６は、ステップＳ４０２において、ｖａｌｕｅ属性が「Ｉｎｔｒｏｄｕｃｅ ａｎ ａｓｓｕｍｐｔｉｏｎ」であるストラテジノードの情報と、ｄｅｓｃｒｉｐｔｉｏｎ属性が「Ａｓｓｕｍｐｔｉｏｎ ｘ：Ｄ」であるコンテキストノードの情報と、そのストラテジノードがｓｏｕｒｃｅであり、そのコンテキストノードがｔａｒｇｅｔであるリンクの情報とを生成する。そして、翻訳部１６は、ステップＳ４０２で生成されたノードはリーフでなく、残り「ｔ」はケースであると判断し、ｔに対しケースに応じた記述の処理を行う（ステップＳ４０３〜Ｓ４０５）。
また、ステップＳ４０１において「→Ｉｎｔｒｏ｛Ｇ_１｝（λ ｈ→ｔ）」のパターンが特定された場合には、翻訳部１６は、ステップＳ４０２おいて、ｖａｌｕｅ属性が「Ａｓｓｕｍｅ ｔｈｅ ａｎｔｅｃｅｄｅｎｔ」であるストラテジノードの情報と、ｄｅｓｃｒｉｐｔｉｏｎ属性が「Ａｓｓｕｍｐｔｉｏｎ ｈ：Ｇ_１」であるコンテキストノードの情報と、そのストラテジノードがｓｏｕｒｃｅであり、そのコンテキストノードがｔａｒｇｅｔであるリンクの情報とを生成する。そして、翻訳部１６は、ステップＳ４０２で生成されたノードはリーフでなく、残り「ｔ」はケースであると判断し、ｔに対しケースに応じた記述の処理を行う（ステップＳ４０３〜Ｓ４０５）。このようにして、図１８の検査対象情報をグラフ情報に翻訳した結果は、図１９で示されるようになる。なお、ストラテジノードにおけるｖａｌｕｅは、それら以外のものであってもよい。但し、∀Ｉｎｔｒｏ｛Ｄ｝のパターンと、→Ｉｎｔｒｏ｛Ｇ_１｝のパターンとで別のものになることが好適である。グラフ情報から検査対象情報への翻訳を適切に行うことができるようにするためである。また、このようにして生成されるコンテキストノードも、他のコンテキストノードと区別可能になっていることが好適である。具体的には、そのコンテキストノードに対応するノードの情報において、ｔｙｐｅを「Ｃｏｎｔｅｘｔ５」とすることによって、その区別が行われるようにしてもよい。なお、∀Ｉｎｔｒｏや→Ｉｎｔｒｏに応じて生成されたストラテジノードをルートノードとするアーギュメントのグラフ情報を検査対象情報に翻訳する際のアーギュメントの処理（図８）は次のようになる。∀Ｉｎｔｒｏや→Ｉｎｔｒｏの処理に応じて生成されたコンテキストノード（例えば、ｔｙｐｅ属性が「Ｃｏｎｔｅｘｔ５」であるノード）のことを、通常のコンテキストノードと区別して「Ａｓｓｕｍｐｔｉｏｎを示すコンテキストノード」と呼ぶことにする。ステップＳ７０３において、リンクのパターンが（ストラテジノード、ゴールノード）または（ストラテジノード、通常のコンテキストノード）である場合は、先に説明した通りに処理を進める。リンクのパターンが（ストラテジノード、Ａｓｓｕｍｐｔｉｏｎを示すコンテキストノード）である場合、コンテキストノードのｄｅｓｃｒｉｐｔｉｏｎ属性は「Ａｓｓｕｍｐｔｉｏｎ ｘ：Ｄ」の形であり、ステップＳ７０６では、これからＡｇｄａの変数名「ｘ」とＳｅｔ型のＡｇｄａ項「Ｄ」を生成し、ステップＳ７０７では演算子を生成しない。ステップＳ７１０では、アーギュメントのルートノードのｖａｌｕｅ属性が「Ｉｎｔｒｏｄｕｃｅ ａｎ ａｓｓｕｍｐｔｉｏｎ」である場合は、ストラテジの項として「∀Ｉｎｔｒｏ｛Ｄ｝」を生成し、「Ａｓｓｕｍｅ ｔｈｅ ａｎｔｅｃｅｄｅｎｔ」である場合は、「→Ｉｎｔｒｏ｛Ｄ｝」を生成する。ここで、「Ｄ」は、Ａｓｓｕｍｐｔｉｏｎを示すコンテキストノードへのリンクのパターンに対してステップＳ７０６で生成した項である。ステップＳ７１１では、アーギュメントの項として、
ＣＯＮＴＥＸＴ［（コンテキストノード項１）／
ＣＯＮＴＥＸＴ［（コンテキストノード項２）／
…
ＣＯＮＴＥＸＴ［（コンテキストノード項ｍ）／
（ステップＳ７１０で生成されたストラテジの項）（λ ｘ→（ケース項））
］…］］
を生成する。ここで、（コンテキストノード項ｉ）は、通常のコンテキストノードへのリンクのパターンに対してステップＳ７０６で生成した項、（ケース項）は、ゴールノードへのリンクのパターンに対してステップＳ７０５で生成した項、「ｘ」は、Ａｓｓｕｍｐｔｉｏｎを示すコンテキストノードへのリンクのパターンに対してステップＳ７０６で生成した変数名である。なお、そのＤ−Ｃａｓｅは、ステップＳ７０５のケースの処理によって生成したものである。このように、上記具体例で説明した以外の他の演算子や項についても、翻訳を行うことができる。また、本実施の形態で説明した以外の項や演算子についても、同様にして、適宜、検査対象情報で使用され、また、検査対象情報からグラフ情報への翻訳、または、グラフ情報から検査対象情報への翻訳が行われてもよいことは言うまでもない。なお、ここで説明したように、項とノードとが対応し、演算子とリンクとが対応するとは限らない。すなわち、翻訳時にはそれら以外の対応関係をも用いて、検査対象情報とグラフ情報との間の翻訳が行われてもよい。
【０１６７】
また、上述した具体例では、Ｅｖｉｄｅｎｃｅ−Ａを、Ｅｖｉｄｅｎｃｅ−Ｂに書き間違えていた場合に、証明検査によってエラーの検出されることについて説明した。そのエラーは、推論規則の適用のしかたの誤りに関するエラーであると言うことができる。ここでは、他の例として、証明検査において、場合分けが適切でないエラーが検出されることについて説明する。まず、モデル情報の一部として、図２０で示されるＭａｃｈｉｎｅｒｙＨａｚａｒｄが検査対象記憶部１１で記憶されているとする。図２０において、「ｄａｔａ ＨａｚａｒｄＴｙｐｅ：Ｓｅｔ ｗｈｅｒｅ」以下において、ＭｅｃｈａｎｉｃａｌからＣｏｍｂｉｎａｔｉｏｎまでの１０個のハザード種別が規定されている。また、その下に、「全てのハザード種別ｔについてＰ（ｔ）」（Ｐはハザード種別を引数にとる述語）という形のゴールを示すための一般的ストラテジ「Ａｒｇｕｅ₋ｏｖｅｒ₋ＨａｚａｒｄＴｙｐｅ」が定義されている。このストラテジは、「ｔがＭｅｃｈａｎｉｃａｌハザードである場合」、「ｔがＥｌｅｃｔｒｉｃａｌハザードである場合」、…等の１０の場合のサブゴールをそれぞれ示すことによってゴールを示すものである。図２１Ａ，図２１Ｂは、検査対象記憶部１１で記憶されている検査対象情報の一部を示す情報である。図２１Ａの５行目において、「ｏｐｅｎ ｉｍｐｏｒｔ ＭａｃｈｉｎｅｒｙＨａｚａｒｄ」と記述されており、この検査対象情報において、図２０のＭａｃｈｉｎｅｒｙＨａｚａｒｄが読み込まれている。また、前述の一般的ストラテジ「Ａｒｇｕｅ₋ｏｖｅｒ₋ＨａｚａｒｄＴｙｐｅ」のパラメータＰ（ｔ）に当たる具体的述語として「ｔ ｈａｚａｒｄｓ₋ａｒｅ₋ｅｘａｍｉｎｅｄ」が定義され、そのｔを具体的なハザード種別「Ｍｅｃｈａｎｉｃａｌ」、「Ｅｌｅｃｔｒｉｃａｌ」、…、「Ｃｏｍｂｉｎａｔｉｏｎ」とした場合の１０のサブゴールに対する１０のサブケースの記述「ｌｅｖｅｌ２−Ｍｅｃｈａｎｉｃａｌ」、「ｌｅｖｅｌ２−Ｅｌｅｃｔｒｉｃａｌ」、…、「ｌｅｖｅｌ２−Ｃｏｍｂｉｎａｔｉｏｎ」が与えられている。また、図２１Ｂにおいて、ストラテジ「Ａｒｇｕｅ₋ｏｖｅｒ₋ＨａｚａｒｄＴｙｐｅ」による１０の場合への場合分けの議論構造情報が具体的に記述されている。その議論構造に対応するグラフ情報は、図２２で示されるものであり、ストラテジノード「Ａｒｇｕ₋ｏｖｅｒ₋ＨａｚａｒｄＴｙｐｅ」の子ノードとして、１０個のハザード種別に対応した１０個のゴールノードが存在している。この図２１Ａ，図２１Ｂで示される検査対象情報について、検査部１２が証明検査を行い、エラーが存在しないことがある時点で確認されたとする。その後、状況の変化に応じて、図２０のＭａｃｈｉｎｅｒｙＨａｚａｒｄの定義において、図２３の矢印の位置で示されるように、ＨａｚａｒｄＴｙｐｅにＴｅｒｒｏｒｉｓｍをさらに追加し、ストラテジ「Ａｒｇｕｅ₋ｏｖｅｒ₋ＨａｚａｒｄＴｙｐｅ」の定義も、１１の場合への場合分けに拡張したが、図２１Ａ，図２１Ｂの議論構造情報を更新し忘れて、検査対象情報に不整合を導入してしまったとする。その後に、もう一度、検査部１２が証明検査を行うと、この場合には、モデル情報におけるＨａｚａｒｄＴｙｐｅにはＴｅｒｒｏｒｉｓｍが含まれるが、議論構造情報にはＴｅｒｒｏｒｉｓｍが含まれていないため、エラーが検出されることになる。その結果、例えば、ユーザが、議論構造情報において、Ｔｅｒｒｏｒｉｓｍに対応する記述を追加することによって、検査対象情報（議論構造情報）を修正し、エラーとならないようにすることができる。このように、証明検査によって、整合性の検査対象であるケースにおける場合分けがあらかじめ規定されている通りに行われているかどうかをチェックすることも可能である。
【０１６８】
次に、上述の説明以外のエラーの例として、証明検査において、数値の単位が異なっているエラーが検出されることについて説明する。まず、モデル情報の一部として、図２４で示される検査対象情報が検査対象記憶部１１で記憶されているとする。この検査対象では、メートル法の重量単位ｋｇ（キログラム）と、ヤード・ポンド法の重量単位ｌｂ（ポンド）とについて、それぞれ異なる型が定義されている。したがって、ケース
ｍｙＷｅｉｇｈｔ ｉｓＬｉｇｈｔｅｒＴｈａｎ １００ ｌｂ∋ｍｙＥｖｉｄｅｎｃｅ
においては、ゴールに含まれる「１００ ｌｂ」について、型が合わないことになる。そのため、この図２４で示される検査対象情報について証明検査を行うと、図２５で示されるように、エラーが検出されることになる。図２５は、検査結果出力部１３が表示した、証明検査の結果を示すものである。図２５の上部では、エラーの箇所に下線が引かれ、その先頭にカーソルが位置することによって、エラーの箇所が明示されている。また、図２５の下から５行目から下から３行目までで示される検査結果のうち、１行目（図２５の下から５行目）を見ることによって、エラーの箇所（ファイル名：行番号，コラム番号）を知ることができ、３行目（図２５の下から３行目）を見ることによって、「１００ ｌｂ」が、期待されるところの型「ＭｅｔｒｉｃＷｅｉｇｈｔ」を持っていることを確認する際にエラーが判明したことを知ることができ、２行目（図２５の下から４行目）を見ることによって、その「１００ ｌｂ」の型であるＩｍｐｅｒｉａｌＷｅｉｇｈｔは、ＭｅｔｒｉｃＷｅｉｇｈｔには変換できない旨のエラーの内容を知ることができる。このように、検査対象情報において、証明検査の対象としたいものについて適宜、型を定義して記述することによって、所望のものを証明検査の対象とすることができる。
【０１６９】
また、Ａｇｄａ言語での正確な記述をする場合には、演算子と引数との間はすべて空白で区切られている必要があり、コロンや等号の前後に空白が必要であるが、上記具体例においては、説明の便宜上、その空白を省略した箇所がある。
【０１７０】
以上のように、本実施の形態による整合性検査装置１によれば、アシュランス・ケースのような整合性の検査対象であるケースの整合性を、証明検査（プルーフチェック）によって自動的に検査することができる。したがって、推論規則の適用のしかたが不適切であったり、あらかじめ規定されている場合分けと異なる場合分けが行われていたり、使用する単位が異なっていたりした場合には、そのエラーを検出することができる。その結果、そのエラーを修正し、整合性を有するケースを構築することができる。また、その自動的な検査を、定理証明支援系を用いて行うことによって、検査を行う独自のソフトウェアを開発する必要がなくなる。また、翻訳部１６によって、人工言語で記述された検査対象情報をグラフ情報に変換することによって、その人工言語による記述に不慣れな者であっても、ケースの構造を容易に把握することができるようになる。また、グラフ情報を検査対象情報に翻訳することも可能であるため、その人工言語に精通していないユーザは、グラフ情報においてケースの編集を行い、その編集後のケースに応じたグラフ情報を検査対象情報に翻訳することによって、人工言語で記述された検査対象情報を生成することも可能である。また、そのようにして翻訳された検査対象情報に対して証明検査を行うことによって、グラフ情報において生成されたケースにエラーが存在するかどうかを確認することもできる。
【０１７１】
また、アシュランス・ケース等の整合性の検査対象であるケースは、最終的にはリーフであるエビデンスによって証明されることになる。したがって、エビデンスが変更された場合などには、その変更後のエビデンスを用いて検査対象情報について証明検査を行うことで、整合性の検査対象であるケースの整合性が担保されているかどうかを簡単に確認することができる。また、そのような場合には、エビデンスを入力データとして、整合性を検査していると考えることもできる。
【０１７２】
なお、本実施の形態では、特に図３〜図８のフローチャートで示される翻訳に関する処理では、ケースが木構造を有する場合について説明したが、前述のように、ケースは、有向非巡回グラフの構造を有してもよい。したがって、ここでは、有向非巡回グラフの構造を有するケースに応じた検査対象情報について説明し、そのような検査対象情報をグラフ情報に翻訳する場合の処理と、また、そのようなグラフ情報を検査対象情報に翻訳する場合の処理とについて説明する。有向非巡回グラフの構造を有する場合には、あるノードが２以上の親ノードを有することになる。その場合には、図２６で示されるように、検査対象情報において、ｌｅｔ構文を用いて共有される部分グラフのルートノード、すなわち、２以上の親ノードを有するノードを共有することを宣言する。なお、そのノードを共有すると言うことは、言い換えれば、そのノードをルートノードとする部分グラフを共有することになる。具体的な記述としては、図２６で示されるように、Ｅｖｉｄｅｎｃｅ−Ａが共有される場合には、そのＥｖｉｄｅｎｃｅ−Ａを「ｍｙＳｈａｒｅＥｖｉｄｅｎｃｅ」と定義する。その定義の次の行に存在するＰｒａｇｍａ｛−＃ ＤＣＡＳＥ ｍｙＳｈａｒｅｄＥｖｉｄｅｎｃｅ ｓｈａｒｅｄ ＃−｝は、部分グラフを共有する旨の宣言であることを示すものである。このＰｒａｇｍａが存在することによって、局所モデル情報等を含むｌｅｔ構文と区別することができる。なお、ｉｎより後の議論構造において、２回、ｍｙＳｈａｒｅＥｖｉｄｅｎｃｅが出てくるが、それらは、ｌｅｔとｉｎとの間で定義した通り、Ｅｖｉｄｅｎｃｅ−Ａである。なお、Ａｇｄａ言語を、検査対象情報を記述する人工言語として用いる具体例においては、ゴールノードやストラテジノード、エビデンスノードが２以上の親ノードを有することは想定しているが、コンテキストノードが２以上の親ノードを有することは想定していない。コンテキストノードが２以上の親ノードを有する場合には、その親ノードのすべてに共通する祖先ノードを、そのコンテキストノードの親ノードとすることによって、コンテキストノードが２以上の親ノードを有さないようにすることができるからである。また、ゴールノードの子ノードとしては、コンテキストノード以外のノードが複数存在することはないものとする。
【０１７３】
このような有向非巡回グラフの構造を有するケースに応じた検査対象情報をグラフ情報に翻訳する場合には、検査対象情報にｌｅｔ構文が存在する場合に、そのｌｅｔ構文がノードの共有のためのものか、それ以外のものかを判断する。その判断は、前述のＰｒａｇｍａを用いて判断することができる。そして、ノードの共有のためのｌｅｔ構文である場合には、翻訳部１６は、ｌｅｔとｉｎとの間で記述されている定義（図２６の例では、「ｍｙＳｈａｒｅＥｖｉｄｅｎｃｅ＝Ｅｖｉｄｅｎｃｅ−Ａ」）を一時的に記憶しておく。そして、ｍｙＳｈａｒｅＥｖｉｄｅｎｃｅの項に対応するノードを生成する処理（ステップＳ３０２，Ｓ４０２）において、翻訳部１６は、すでにそのノードが存在するかどうか判断し、まだ存在しない場合には、その定義に応じてノードの生成を行う。一方、すでに存在する場合には、そのノードの生成を行わず、上位のフローチャートに戻るようにしてもよい。そのようにすることで、共有されているノードに応じた項が１回目に出てきたときには、通常通り、その項に対応するノードが生成されるが、その項の２回目以降の出現に対しては、ノード自体は生成されず、１回目の出現の際に生成されたノードへのリンクのみが生成されることになる。図２６で示される検査対象情報が翻訳されたグラフ情報は、図２７で示されるようになる。図２７において、Ｅｖｉｄｅｎｃｅ−Ａのノードが共有されていることが分かる。
【０１７４】
次に、図２７に応じたグラフ情報を検査対象情報に翻訳する場合の処理について説明する。この場合には、翻訳部１６は、グラフ情報を参照し、共有されているノード、すなわち、親ノードを２以上有するノード（例えば、Ｅｖｉｄｅｎｃｅ−Ａのノード）が存在するかどうか判断する。具体的には、翻訳部１６は、あるノードをｔａｒｇｅｔノードとする２以上のリンクの情報が存在する場合に、共有されているノードが存在すると判断してもよい。その場合には、２以上のリンクの情報によってｔａｒｇｅｔノードとされているノードが、共有されているノードとなる。そして、翻訳部１６は、その共有されているノード以下の部分グラフに応じた項について、新たな名前（例えば、「ｓｈａｒｅｄＥｖｉｄｅｎｃｅ」など）を付ける定義（例えば、「ｓｈａｒｅｄＥｖｉｄｅｎｃｅ＝Ｅｖｉｄｅｎｃｅ−Ａ」など）を生成する。その名前は、例えば、「ｓｈａｒｅｄ」と、ノードの種類を示す情報（例えば、「Ｇｏａｌ」や「Ｓｔｒａｔｅｇｙ」、「Ｅｖｉｄｅｎｃｅ」など）とをつなげたものであってもよい。また、その名称が重複する場合（例えば、共有されるエビデンスノードが２以上存在する場合など）には、その名前の最後に、適宜、「１」や「２」等の情報を付加してもよい。次に、翻訳部１６は、その定義を挿入する位置（ノード）を特定する。その特定対象となるノードは、
（条件１）ルートノードからの経路が一通りである
（条件２）そのノードの子ノードに、共有されているノードの祖先であるものが２以上存在する
という２個の条件を満たすノードである。その特定対象のノードを特定する方法として、例えば、次のような処理を行ってもよい。まず、判断対象のノードをルートノードとする。また、判断対象のノードの子ノードに、共有されているノードの祖先であるノードが１個存在するのか、あるいは、２個以上存在するのか判断する。そして、２個以上存在する場合には、判断対象のノードが特定対象のノードとなる。一方、１個存在する場合には、その１個のノード（このノードは、ルートノードの子ノードである）を判断対象のノードとする。また、前述の処理と同様に、その判断対象のノードの子ノードに、共有されているノードの祖先であるノードが１個存在するのか、あるいは、２個以上存在するのか判断する。そして、２個以上存在する場合には、判断対象のノードが特定対象のノードとなる。一方、１個存在する場合には、その１個のノードを判断対象のノードとする。この処理を、判断対象のノードが特定対象のノードとなるまで繰り返して実行すればよいことになる。そして、特定対象のノードが特定できた後には、前述の説明と同様に、グラフ情報から検査対象情報を生成する処理を行う。その際に、共有されているノードについては、定義した名称の項を生成するものとする。また、図６で示される検査対象への翻訳の処理が終了した後に、特定対象ノード以下の部分グラフに応じた項「ｔ」を、あらかじめ生成していた共有部分グラフに応じた項の定義「ｓｈａｒｅｄＥｖｉｄｅｎｃｅ＝（共有部分グラフの項）」を含むｌｅｔ構文の項で置き換える。具体的には、項ｔを、項
ｌｅｔ
ｓｈａｒｅｄＥｖｉｄｅｎｃｅ＝（共有部分グラフの項）
｛−＃ ＤＣＡＳＥ ｓｈａｒｅｄＥｖｉｄｅｎｃｅ ｓｈａｒｅｄ ＃−｝
ｉｎ
ｔ
で置き換える。このようにして、有向非巡回グラフの構造を有するグラフ情報から検査対象情報への翻訳を行うことができる。なお、検査対象情報におけるｌｅｔ構文の生成は、検査対象情報において順次、項や演算子を追加する際に行ってもよい。すなわち、特定対象のノードに応じた項が生成された時点で、共有部分グラフに応じた項の定義を含むｌｅｔ構文を生成し、さらに、それ以降の項や演算子の生成の処理を継続するようにしてもよい。ここで、図２６，図２７の例の場合には、特定対象のノードは、ｔｏｐＳｔｒａｇｅｇｙに応じたストラテジノードである。
【０１７５】
また、本実施の形態において、メタ変数を用いることによって、整合性の検査対象であるケースに応じた未完成の検査対象情報や未完成のグラフ情報についても証明検査を行うようにしてもよい。そのためには、検査対象情報を記述する人工言語として、対話型証明支援系の人工言語を用いることが好適である。これは、対話型証明支援系の人工言語であれば、検査部１２が、メタ変数を含む項を有する検査対象情報についても証明検査（プルーフチェック）を行うことができるからである。なお、前述のＡｇｄａ言語は、対話型証明支援系の人工言語の一例である。ここで、メタ変数とは、未完成（作成途中）の項の中で、最終的には正式な記述がなされる部分を示すプレースホールダ、すなわち、「この部分は、今は未定の穴開き状態であるが、将来は具体的な部分項で埋められる部分である」という部分を示すプレースホールダである。なお、そのメタ変数を含む検査対象情報は、グラフ情報から翻訳されたものであってもよく、あるいは、そうでなくてもよい。後者の場合としては、例えば、ユーザが検査対象情報を人工言語での記述として入力する際に、メタ変数を用いる場合があり得る。このように、メタ変数を用いて記述された検査対象情報について証明検査を行うことによって、作成途中の検査対象情報（あるいは、その検査対象情報の翻訳元の作成途中のグラフ情報）に誤りがあるかどうかを確認することができ、誤りがある場合には、適宜、その誤りを解消するように検査対象情報（あるいは、その検査対象情報の翻訳元のグラフ情報）を修正することができる。したがって、メタ変数を含む検査対象情報の証明検査は、検査対象情報に変更が加えられるごとに行われることが好適である。また、グラフ情報が作成されている場合には、作成途中のグラフ情報に変更が加えられるごとに、翻訳と、その翻訳後のメタ変数の項を含む検査対象情報の証明検査とが行われることが好適である。なお、メタ変数を含んだ検査対象情報の証明検査については、次の情報を参照されたい。
情報：Ｕｌｆ Ｎｏｒｅｌｌ．Ｔｙｐｅ ｃｈｅｃｋｉｎｇ ｉｎ ｔｈｅ ｐｒｅｓｅｎｃｅ ｏｆ ｍｅｔａ−ｖａｒｉａｂｌｅｓ．Ｉｎ ＴＹＰＥＳ ２００７，Ｃｉｖｉｄａｌｅ ｄｅｌ Ｆｒｉｕｌｉ，Ｉｔａｌｙ，２００７年５月
（ｃｏｎｆｅｒｅｎｃｅ ｕｒｌ：ｈｔｔｐ：／／ｕｓｅｒｓ．ｄｉｍｉ．ｕｎｉｕｄ．ｉｔ／ｔｙｐｅｓ０７／）
情報：Ｃａｔａｒｉｎａ Ｃｏｑｕａｎｄ ａｎｄ Ｔｈｉｅｒｒｙ Ｃｏｑｕａｎｄ．Ｓｔｒｕｃｔｕｒｅｄ ｔｙｐｅ ｔｈｅｏｒｙ． Ｉｎ Ｗｏｒｋｓｈｏｐ ｏｎ Ｌｏｇｉｃａｌ Ｆｒａｍｅｗｏｒｋｓ ａｎｄ Ｍｅｔａ−ｌａｎｇｕａｇｅｓ，Ｐａｒｉｓ，Ｆｒａｎｃｅ，１９９９年９月
（ｗｏｒｋｓｈｏｐ ｕｒｌ： ｈｔｔｐ：／／ｗｗｗ．ｓｉｔｅ．ｕｏｔｔａｗａ．ｃａ／〜ａｆｅｌｔｙ／ＬＦＭ９９／ｉｎｄｅｘ．ｈｔｍｌ）
【０１７６】
ここで、メタ変数を含む検査対象情報や、グラフ情報の例について簡単に説明する。図２８は、メタ変数を含む検査対象情報の一例である。図２８において、メタ変数｛！！｝が用いられている。したがって、この場合には、ゴールノードの項「ＴｏｐＧｏａｌ」以下が未定である。なお、図２８の検査対象情報は、図２９に応じたグラフ情報が翻訳されたものであると考えてもよい。図２９では、ゴールノードの子ノード側が未定であるため、ｖａｌｕｅ＝"？"を有するエビデンスノードが設定されている。翻訳部１６は、ｖａｌｕｅ＝"？"を有するエビデンスノードを、メタ変数｛！！｝の項に変換するものとする。なお、検査部１２が、図２８の検査対象情報について証明検査を行ったとしても、エラーは検出されない。その証明検査は、対話型証明支援系のプルーフチェッカーによる証明検査である。
【０１７７】
次に、ユーザが、ゴールノードの項「ＴｏｐＧｏａｌ」に対して、ストラテジノードの項等を新たに設定し、検査対象情報が図３０で示されるようになったとする。なお、この場合にも、ユーザが、Ｄ−Ｃａｓｅ Ｅｄｉｔｏｒ等を用いてグラフ情報を変更し、その結果、図３１に応じたグラフ情報が生成され、そのグラフ情報の翻訳結果が図３０で示される検査対象情報であると考えてもよい。図３０の検査対象情報では、サブゴールノードの項「ＳｕｂＧｏａｌ−Ａ」、「ＳｕｂＧｏａｌ−Ｂ」以下が未定であり、その箇所にメタ変数｛！！｝がそれぞれ設定されている。この場合にも、図３０の検査対象情報について証明検査が行われても、エラーは検出されない。
【０１７８】
さらに、ユーザが、サブゴールノードの項「ＳｕｂＧｏａｌ−Ａ」に対して、エビデンスノードの項「Ｅｖｉｄｅｎｃｅ−Ａ」を新たに設定し、検査対象情報が図３２のようになったとする。なお、この場合にも、ユーザが、Ｄ−Ｃａｓｅ Ｅｄｉｔｏｒ等を用いてグラフ情報を変更し、その結果、図３３に応じたグラフ情報が生成され、そのグラフ情報の翻訳結果が図３２で示される検査対象情報であると考えてもよい。この場合にも、図３２の検査対象情報について証明検査が行われても、エラーは検出されない。
【０１７９】
一方、ユーザが、図３０で示される検査対象情報において、図３４で示されるように、サブゴールノードの項「ＳｕｂＧｏａｌ−Ａ」に対応したエビデンスノードの項として、「Ｅｖｉｄｅｎｃｅ−Ｂ」を入力しようとしたとする。この場合には、ＳｕｂＧｏａｌ−Ａと、Ｅｖｉｄｅｎｃｅ−Ｂとの型が異なるため、検査部１２は、証明検査の結果としてエラーを返し、入力の受け付けを拒否する。そして、ユーザは、検査結果出力部１３が表示した図３５の下部３行で示される検査結果を見ることによって、エラーの箇所（一行目に記述されている「ファイル名：行番号，コラム番号」）と、そのエラーの内容（三行目に記述されている「（入力された項）Ｅｖｉｄｅｎｃｅ−Ｂが（期待されるところの）型ＳｕｂＧｏａｌ−Ａを持っていることを確認する際にエラーが判明した」、二行目に記述されている「（入力された項の型）ＳｕｂＧｏａｌ−Ｂは、ＳｕｂＧｏａｌ−Ａには変換できない（両者をＳｅｔ型の要素と見たとき）」）とを知ることができるようになる。その結果、ユーザは、そのエラーを解消するために、検査対象情報を図３２で示されるように変更することができる。なお、メタ変数に入れようとする項は、メタ変数を含んでいてもよく、あるいは、含んでいなくてもよい。図３４では、メタ変数を含むエビデンスノードの項「Ｅｖｉｄｅｎｃｅ−Ｂ」が設定されている場合について示している。
【０１８０】
ユーザが、人工言語での記述において、メタ変数に型の合わない項を入力しようとする場合は上のように入力操作自体が拒否されるが、Ｄ−Ｃａｓｅ Ｅｄｉｔｏｒ等での誤った図的編集は、それ自体は拒否されず、翻訳を経て証明検査をした時点で誤りが判明する。この場合でも、未完成のケースの整合性を検査できることにより、早い段階で誤りを見つけることができる。ユーザが、図３１に応じたグラフ情報において、図３６で示されるように、サブゴールノード「ＳｕｂＧｏａｌ−Ａ」に対応したエビデンスノードとして、「Ｅｖｉｄｅｎｃｅ−Ｂ」を設定したとする。ユーザは、ケースが未完成なまま、そのグラフ情報を、翻訳部１６によって、図３７で示される検査対象情報に翻訳できる。この場合にも、ＳｕｂＧｏａｌ−Ａと、Ｅｖｉｄｅｎｃｅ−Ｂとの型が異なるため、検査部１２は、証明検査の結果としてエラーを返す。そして、ユーザは、検査結果出力部１３が表示した図３８で示される検査結果を見ることによって、エラーの箇所と、そのエラーの内容とを知ることができるようになる。その結果、ユーザは、そのエラーを解消するために、検査対象情報を図３２で示されるように変更することができる。
【０１８１】
上記説明のように、検査対象情報において、メタ変数を含む項の記載を許容し、そのメタ変数を含む検査対象情報についても証明検査を行うことによって、作成途中の検査対象情報や、作成途中のグラフ情報に誤りがあるかどうかを確認することができる。そして、誤りがあれば、それを訂正することによって、適切な検査対象情報やグラフ情報にすることができる。一方、誤りがなければ、その後に適切に検査対象情報やグラフ情報を構築することによって、誤りのない検査対象情報やグラフ情報を構築できる可能性のあることを知ることができる。なお、上記説明において、グラフ情報から検査対象情報への翻訳時のモデル情報の取り扱いについて特に言及しなかったが、そのモデル情報は、前述のように、例えば、グラフ情報において不可視情報として存在し、その不可視情報であるモデル情報が検査対象情報に含まれるようになってもよく、グラフ情報において、コンテキストノードの内容によってモデル情報が設定され、そのモデル情報が検査対象情報に含まれるようになってもよく、または、グラフ情報から検査対象情報への翻訳時にはモデル情報が生成されず、その翻訳の後に、モデル情報を別途に人工言語での記述として入力するようにしてもよい。また、上記説明においては、メタ変数を含むグラフ情報としては、メタ変数のみからなるエビデンスノードを持つグラフ情報について説明したが、そうでなくてもよい。例えば、ゴールノードあるいはストラテジノードの項がメタ変数であってもよく、またはそれらの項自体はメタ変数でなくそれらの項の一部としてメタ変数が現れてもよい。またあるいは、グラフ情報の構成要素としてノードとリンクだけでなく「部分グラフ」も認めるグラフ情報の表記において、メタ変数を未確定部分グラフに対応付けることによって、「未確定アーギュメント」や「未確定ケース」を扱ってもよい。また、上記説明で参照した一連の各検査対象情報において、検査対象情報ごとにモジュール名が異なっていたり、検査対象情報ごとに異なるコメントが記載されていたりするが、それらは時系列中の時点々々での様態を記録するための便宜上のものであり、同じモジュール名が使用され、コメントが存在しないと考えてもよい。
【０１８２】
また、本実施の形態による整合性検査装置１では、実行部１４を備え、検査対象情報を実行する場合について説明したが、そうでなくてもよい。検査対象情報に関する実行を行わなくてもよい場合には、整合性検査装置１は、実行部１４を備えていなくてもよい。また、検査対象情報に関する実行を行わない場合には、検査対象情報は、構成的型理論ではない型理論に基づく人工言語で記述されたものであってもよい。
【０１８３】
また、本実施の形態では、検査対象情報からグラフ情報への翻訳と、グラフ情報から検査対象情報への翻訳との両方を行う場合について説明したが、そうでなくてもよい。翻訳部１６は、いずれか一方の翻訳を行うものであってもよい。また、翻訳を行わなくてもよい場合には、整合性検査装置１は、翻訳部１６やグラフ記憶部１５を備えていなくてもよい。
【０１８４】
また、本実施の形態では、整合性検査装置１が表示部１７や受付部１８を備える構成について説明したが、そうでなくてもよい。整合性検査装置１が表示部１７を有さない場合には、整合性検査装置１は、例えば、検査対象記憶部１１で記憶されている検査対象情報にエラーが存在するかどうかを検査するためだけの装置であってもよい。また、整合性検査装置１が受付部１８を有さない場合には、整合性検査装置１は、例えば、外部から着脱可能な記録媒体等によって提供された検査対象情報にエラーが存在するかどうかを検査する装置であってもよい。
【０１８５】
また、本実施の形態で説明したノードの種類、演算子や項の種類は一例であり、それら以外のノードの種類や、演算子や項の種類が存在してもよいことは言うまでもない。また、アシュランス・ケース等の整合性の検査対象であるケースが有する情報のうち、Ａｇｄａ等の人工言語で記述する範囲、すなわち、検査対象情報で記述する範囲を多くすればするほど、整合性の検査対象もより広がることになる。したがって、より多くの範囲を検査対象情報において記述することが好適である。
【０１８６】
また、本実施の形態では、モデル情報がｐｏｓｔｕｌａｔｅの宣言のみを有する場合について主に説明したが、モデル情報には、それ以外の宣言が含まれてもよいことは言うまでもない。モデル情報は、例えば、ｐｏｓｔｕｌａｔｅ以外の種類の宣言である、データ型定義、レコード型定義、関数定義、または、他のモジュールのインポート宣言等を含んでいてもよい。
【０１８７】
また、上記実施の形態では、整合性検査装置１がスタンドアロンである場合について説明したが、整合性検査装置１は、スタンドアロンの装置であってもよく、サーバ・クライアントシステムにおけるサーバ装置であってもよい。後者の場合には、出力部や表示部、受付部は、通信回線を介して情報を出力したり、情報を表示したり、入力を受け付けたりしてもよい。
【０１８８】
また、上記実施の形態において、各処理または各機能は、単一の装置または単一のシステムによって集中処理されることによって実現されてもよく、あるいは、複数の装置または複数のシステムによって分散処理されることによって実現されてもよい。
【０１８９】
また、上記実施の形態において、各構成要素間で行われる情報の受け渡しは、例えば、その情報の受け渡しを行う２個の構成要素が物理的に異なるものである場合には、一方の構成要素による情報の出力と、他方の構成要素による情報の受け付けとによって行われてもよく、あるいは、その情報の受け渡しを行う２個の構成要素が物理的に同じものである場合には、一方の構成要素に対応する処理のフェーズから、他方の構成要素に対応する処理のフェーズに移ることによって行われてもよい。
【０１９０】
また、上記実施の形態において、各構成要素が実行する処理に関係する情報、例えば、各構成要素が受け付けたり、取得したり、選択したり、生成したり、送信したり、受信したりした情報や、各構成要素が処理で用いるしきい値や数式、アドレス等の情報等は、上記説明で明記していない場合であっても、図示しない記録媒体において、一時的に、あるいは長期にわたって保持されていてもよい。また、その図示しない記録媒体への情報の蓄積を、各構成要素、あるいは、図示しない蓄積部が行ってもよい。また、その図示しない記録媒体からの情報の読み出しを、各構成要素、あるいは、図示しない読み出し部が行ってもよい。
【０１９１】
また、上記実施の形態において、各構成要素等で用いられる情報、例えば、各構成要素が処理で用いるしきい値やアドレス、各種の設定値等の情報がユーザによって変更されてもよい場合には、上記説明で明記していない場合であっても、ユーザが適宜、それらの情報を変更できるようにしてもよく、あるいは、そうでなくてもよい。それらの情報をユーザが変更可能な場合には、その変更は、例えば、ユーザからの変更指示を受け付ける図示しない受付部と、その変更指示に応じて情報を変更する図示しない変更部とによって実現されてもよい。その図示しない受付部による変更指示の受け付けは、例えば、入力デバイスからの受け付けでもよく、通信回線を介して送信された情報の受信でもよく、所定の記録媒体から読み出された情報の受け付けでもよい。
【０１９２】
また、上記実施の形態において、整合性検査装置１に含まれる２以上の構成要素が通信デバイスや入力デバイス等を有する場合に、２以上の構成要素が物理的に単一のデバイスを有してもよく、あるいは、別々のデバイスを有してもよい。
【０１９３】
また、上記実施の形態において、各構成要素は専用のハードウェアにより構成されてもよく、あるいは、ソフトウェアにより実現可能な構成要素については、プログラムを実行することによって実現されてもよい。例えば、ハードディスクや半導体メモリ等の記録媒体に記録されたソフトウェア・プログラムをＣＰＵ等のプログラム実行部が読み出して実行することによって、各構成要素が実現され得る。なお、上記実施の形態における整合性検査装置１を実現するソフトウェアは、以下のようなプログラムである。つまり、このプログラムは、目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部にアクセス可能なコンピュータを、検査対象情報に対して証明検査を行う検査部、検査部による証明検査の結果を出力する検査結果出力部として機能させるためのプログラムである。
【０１９４】
なお、上記プログラムにおいて、上記プログラムが実現する機能には、ハードウェアでしか実現できない機能は含まれない。例えば、情報を出力する出力部などにおけるモデムやインターフェースカードなどのハードウェアでしか実現できない機能は、上記プログラムが実現する機能には少なくとも含まれない。
【０１９５】
また、このプログラムは、サーバなどからダウンロードされることによって実行されてもよく、所定の記録媒体（例えば、ＣＤ−ＲＯＭなどの光ディスクや磁気ディスク、半導体メモリなど）に記録されたプログラムが読み出されることによって実行されてもよい。また、このプログラムは、プログラムプロダクトを構成するプログラムとして用いられてもよい。
【０１９６】
また、このプログラムを実行するコンピュータは、単数であってもよく、複数であってもよい。すなわち、集中処理を行ってもよく、あるいは分散処理を行ってもよい。
【０１９７】
図３９は、上記プログラムを実行して、上記実施の形態による整合性検査装置１を実現するコンピュータの外観の一例を示す模式図である。上記実施の形態は、コンピュータハードウェア及びその上で実行されるコンピュータプログラムによって実現されうる。
【０１９８】
図３９において、コンピュータシステム９００は、ＣＤ−ＲＯＭ（Ｃｏｍｐａｃｔ Ｄｉｓｋ Ｒｅａｄ Ｏｎｌｙ Ｍｅｍｏｒｙ）ドライブ９０５、ＦＤ（Ｆｌｏｐｐｙ（登録商標） Ｄｉｓｋ）ドライブ９０６を含むコンピュータ９０１と、キーボード９０２と、マウス９０３と、モニタ９０４とを備える。
【０１９９】
図４０は、コンピュータシステム９００の内部構成を示す図である。図４０において、コンピュータ９０１は、ＣＤ−ＲＯＭドライブ９０５、ＦＤドライブ９０６に加えて、ＭＰＵ（Ｍｉｃｒｏ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）９１１と、ブートアッププログラム等のプログラムを記憶するためのＲＯＭ９１２と、ＭＰＵ９１１に接続され、アプリケーションプログラムの命令を一時的に記憶すると共に、一時記憶空間を提供するＲＡＭ（Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ）９１３と、アプリケーションプログラム、システムプログラム、及びデータを記憶するハードディスク９１４と、ＭＰＵ９１１、ＲＯＭ９１２等を相互に接続するバス９１５とを備える。なお、コンピュータ９０１は、ＬＡＮやＷＡＮ等への接続を提供する図示しないネットワークカードを含んでいてもよい。
【０２００】
コンピュータシステム９００に、上記実施の形態による整合性検査装置１の機能を実行させるプログラムは、ＣＤ−ＲＯＭ９２１、またはＦＤ９２２に記憶されて、ＣＤ−ＲＯＭドライブ９０５、またはＦＤドライブ９０６に挿入され、ハードディスク９１４に転送されてもよい。これに代えて、そのプログラムは、図示しないネットワークを介してコンピュータ９０１に送信され、ハードディスク９１４に記憶されてもよい。プログラムは実行の際にＲＡＭ９１３にロードされる。なお、プログラムは、ＣＤ−ＲＯＭ９２１やＦＤ９２２、またはネットワークから直接、ロードされてもよい。
【０２０１】
プログラムは、コンピュータ９０１に、上記実施の形態による整合性検査装置１の機能を実行させるオペレーティングシステム（ＯＳ）、またはサードパーティプログラム等を必ずしも含んでいなくてもよい。プログラムは、制御された態様で適切な機能（モジュール）を呼び出し、所望の結果が得られるようにする命令の部分のみを含んでいてもよい。コンピュータシステム９００がどのように動作するのかについては周知であり、詳細な説明は省略する。
【０２０２】
また、本発明は、以上の実施の形態に限定されることなく、種々の変更が可能であり、それらも本発明の範囲内に包含されるものであることは言うまでもない。
【産業上の利用可能性】
【０２０３】
以上より、本発明による整合性検査装置等によれば、整合性の検査対象であるケースの整合性を自動的に検査できるという効果が得られ、そのような検査を行う装置等として有用である。
【符号の説明】
【０２０４】
１ 整合性検査装置
１１ 検査対象記憶部
１２ 検査部
１３ 検査結果出力部
１４ 実行部
１５ グラフ記憶部
１６ 翻訳部
１７ 表示部
１８ 受付部

【特許請求の範囲】
【請求項１】
目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部と、
前記検査対象情報に対して証明検査を行う検査部と、
前記検査部による証明検査の結果を出力する検査結果出力部と、を備えた整合性検査装置。
【請求項２】
前記検査対象情報は、当該検査対象情報に含まれる各項の定義を含むモデル情報と、当該検査対象情報に対応する有向非巡回グラフの構造を示す議論構造情報とを有する、請求項１記載の整合性検査装置。
【請求項３】
前記検査対象情報に対応する有向非巡回グラフの各ノードと、ノード間の親子関係とを示す情報であり、整合性の検査対象であるケースの情報であるグラフ情報が記憶されるグラフ記憶部と、
前記グラフ情報の各ノードの親子関係のパターンに応じて、前記グラフ情報の各ノードを項に変換し、各ノードの親子関係を演算子に変換し、変換後の検査対象情報を前記検査対象記憶部に蓄積する翻訳部と、をさらに備えた、請求項１または請求項２記載の整合性検査装置。
【請求項４】
前記有向非巡回グラフには、前記整合性の検査対象であるケースに関する文脈情報に対応するコンテキストノードがさらに含まれ、
前記検査対象情報に対応する有向非巡回グラフの各ノードと、ノード間の親子関係とを示す情報であり、整合性の検査対象であるケースの情報であるグラフ情報が記憶されるグラフ記憶部と、
前記検査対象情報を、項と演算子とのパターンに応じて、前記検査対象情報の各項をノードに変換し、各演算子を各ノードの親子関係に変換し、変換後のグラフ情報を前記グラフ記憶部に蓄積する翻訳部と、をさらに備えた、請求項１または請求項２記載の整合性検査装置。
【請求項５】
前記人工言語は、構成的型理論に基づく人工言語である、請求項１から請求項４のいずれか記載の整合性検査装置。
【請求項６】
前記検査部による証明検査によって、エラーのないことが検査された前記検査対象情報を実行する実行部をさらに備えた、請求項５記載の整合性検査装置。
【請求項７】
前記実行部は、前記検査対象情報を実行することにより、当該検査対象情報から、整合性の検査対象であるケースの各ノードに応じた項と、各ノードの親子関係に応じた演算子とを陽に記述する形式の検査対象情報を生成する、請求項６記載の整合性検査装置。
【請求項８】
前記検査対象記憶部では、前記検査対象情報を前記グラフ情報に変換する処理に応じた変換プログラムも記憶され、
前記翻訳部は、前記変換プログラムを実行することによって、前記検査対象情報を前記グラフ情報に変換する、請求項４記載の整合性検査装置。
【請求項９】
前記検査対象情報と前記変換プログラムとは、構成的型理論に基づく同じ人工言語で記述されている、請求項８記載の整合性検査装置。
【請求項１０】
前記検査対象情報の項は、メタ変数を含むものであり、
前記人工言語は、対話型証明支援系の人工言語である、請求項１から請求項９のいずれか記載の整合性検査装置。
【請求項１１】
目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部と、検査部と、検査結果出力部とを用いて処理される整合性検査方法であって、
前記検査部が、前記検査対象情報に対して証明検査を行う検査ステップと、
前記検査結果出力部が、前記検査ステップにおける証明検査の結果を出力する検査結果出力ステップと、を備えた整合性検査方法。
【請求項１２】
目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部にアクセス可能なコンピュータを、
前記検査対象情報に対して証明検査を行う検査部、
前記検査部による証明検査の結果を出力する検査結果出力部として機能させるためのプログラム。

【図１】

【図２】

【図３】

【図４】

【図５】

【図６】

【図７】

【図８】

【図９】

【図１０】

【図１１】

【図１２Ａ】

【図１２Ｂ】

【図１３】

【図１４】

【図１５】

【図１６】

【図１７Ａ】

【図１７Ｂ】

【図１８】

【図１９】

【図２０】

【図２１Ａ】

【図２１Ｂ】

【図２２】

【図２３】

【図２４】

【図２５】

【図２６】

【図２７】

【図２８】

【図２９】

【図３０】

【図３１】

【図３２】

【図３３】

【図３４】

【図３６】

【図３７】

【図３８】

【図３９】

【図４０】

【図３５】

【公開番号】特開２０１３−５４６１６（Ｐ２０１３−５４６１６Ａ）
【公開日】平成２５年３月２１日（２０１３．３．２１）
【国際特許分類】
【出願番号】特願２０１１−１９３４５２（Ｐ２０１１−１９３４５２）
【出願日】平成２３年９月６日（２０１１．９．６）
【国等の委託研究の成果に係る記載事項】（出願人による申告）平成２２年度、独立行政法人科学技術振興機構　研究成果最適展開支援事業　本格研究開発　ハイリスク挑戦タイプの「モデル化技術によるＭＣＵ仕様検証と機能検証の自動化」受託研究、産業技術力強化法第１９条の適用を受ける特許出願
【出願人】（３０１０２１５３３）独立行政法人産業技術総合研究所 (6,529)
【Ｆターム（参考）】