"目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部と、前記検査対象情報に対して証明検査を行う検査部と、前記検査部による証明検査の結果を出力する検査結果出力部と、を備えた整合性検査装置。前記検査対象情報は、当該検査対象情報に含まれる各項の定義を含むモデル情報と、当該検査対象情報に対応する有向非巡回グラフの構造を示す議論構造情報とを有する、請求項1記載の整合性検査装置。前記検査対象情報に対応する有向非巡回グラフの各ノードと、ノード間の親子関係とを示す情報であり、整合性の検査対象であるケースの情報であるグラフ情報が記憶されるグラフ記憶部と、前記グラフ情報の各ノードの親子関係のパターンに応じて、前記グラフ情報の各ノードを項に変換し、各ノードの親子関係を演算子に変換し、変換後の検査対象情報を前記検査対象記憶部に蓄積する翻訳部と、をさらに備えた、請求項1または請求項2記載の整合性検査装置。前記有向非巡回グラフには、前記整合性の検査対象であるケースに関する文脈情報に対応するコンテキストノードがさらに含まれ、前記検査対象情報に対応する有向非巡回グラフの各ノードと、ノード間の親子関係とを示す情報であり、整合性の検査対象であるケースの情報であるグラフ情報が記憶されるグラフ記憶部と、前記検査対象情報を、項と演算子とのパターンに応じて、前記検査対象情報の各項をノードに変換し、各演算子を各ノードの親子関係に変換し、変換後のグラフ情報を前記グラフ記憶部に蓄積する翻訳部と、をさらに備えた、請求項1または請求項2記載の整合性検査装置。前記人工言語は、構成的型理論に基づく人工言語である、請求項1から請求項4のいずれか記載の整合性検査装置。前記検査部による証明検査によって、エラーのないことが検査された前記検査対象情報を実行する実行部をさらに備えた、請求項5記載の整合性検査装置。前記実行部は、前記検査対象情報を実行することにより、当該検査対象情報から、整合性の検査対象であるケースの各ノードに応じた項と、各ノードの親子関係に応じた演算子とを陽に記述する形式の検査対象情報を生成する、請求項6記載の整合性検査装置。前記検査対象記憶部では、前記検査対象情報を前記グラフ情報に変換する処理に応じた変換プログラムも記憶され、前記翻訳部は、前記変換プログラムを実行することによって、前記検査対象情報を前記グラフ情報に変換する、請求項4記載の整合性検査装置。前記検査対象情報と前記変換プログラムとは、構成的型理論に基づく同じ人工言語で記述されている、請求項8記載の整合性検査装置。前記検査対象情報の項は、メタ変数を含むものであり、前記人工言語は、対話型証明支援系の人工言語である、請求項1から請求項9のいずれか記載の整合性検査装置。目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部と、検査部と、検査結果出力部とを用いて処理される整合性検査方法であって、前記検査部が、前記検査対象情報に対して証明検査を行う検査ステップと、前記検査結果出力部が、前記検査ステップにおける証明検査の結果を出力する検査結果出力ステップと、を備えた整合性検査方法。目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部にアクセス可能なコンピュータを、前記検査対象情報に対して証明検査を行う検査部、前記検査部による証明検査の結果を出力する検査結果出力部として機能させるためのプログラム。しかしながら、アシュランスケースは、通常、何万ページにもなる膨大な文書であり、文書の整合性があちらこちらで破れてしまうことがあった。また、その整合性の検査を人手で行うのは非常に困難である。さらに、アシュランスケースは前述のように、プラントや飛行機等の種々のものを対象とするため、一のアシュランスケースを検査するための専用のソフトウェアを開発したとしても、それによって他のアシュランスケースを検査できないこともある。そのような場合には、アシュランスケースの対象ごとに検査のソフトウェアを開発する必要があり、コストが多大になる。また、アシュランスケースの表記方法が変更された場合には、それに応じて、その検査のためのソフトウェアも変更しなければならないという問題もある。一般的に言えば、アシュランスケースのような整合性の検査対象であるケースの整合性を、汎用性の高い方法で精度よく自動的に検査することが求められていた。本発明は、上記課題を解決するためになされたものであり、整合性の検査対象であるケースの整合性を自動的に検査することができる整合性検査装置等を提供することを目的とする。上記目的を達成するため、本発明による整合性検査装置は、目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部と、検査対象情報に対して証明検査を行う検査部と、検査部による証明検査の結果を出力する検査結果出力部と、を備えたものである。このような構成により、整合性の検査対象であるケースを人工言語によって記述することにより、証明検査によって自動的に検査することができるようになる。したがって、検査対象が膨大な量であったとしても、その検査を容易に行うことができる。また、その検査を証明検査、すなわち、定理証明支援系によるプルーフチェッカーによる検査によって行うため、検査のためのソフトウェアを独自に開発する必要もなく、汎用性の高い方法で検査を行うことができる。また、本発明による整合性検査装置では、検査対象情報は、検査対象情報に含まれる各項の定義を含むモデル情報と、検査対象情報に対応する有向非巡回グラフの構造を示す議論構造情報とを有してもよい。また、本発明による整合性検査装置では、検査対象情報に対応する有向非巡回グラフの各ノードと、ノード間の親子関係とを示す情報であり、整合性の検査対象であるケースの情報であるグラフ情報が記憶されるグラフ記憶部と、グラフ情報の各ノードの親子関係のパターンに応じて、グラフ情報の各ノードを項に変換し、各ノードの親子関係を演算子に変換し、変換後の検査対象情報を検査対象記憶部に蓄積する翻訳部と、をさらに備えてもよい。このような構成により、グラフを用いて記述されたケースを検査対象情報に変換し、証明検査を行うことができるようになる。したがって、例えば、人工言語に不慣れな者であっても、人工言語よりも扱いやすいグラフを用いて整合性の検査対象であるケースを記述することによって、そのケースに応じた証明検査の結果を得ることができるようになる。また、本発明による整合性検査装置では、有向非巡回グラフには、整合性の検査対象であるケースに関する文脈情報に対応するコンテキストノードがさらに含まれ、検査対象情報に対応する有向非巡回グラフの各ノードと、ノード間の親子関係とを示す情報であり、整合性の検査対象であるケースの情報であるグラフ情報が記憶されるグラフ記憶部と、検査対象情報を、項と演算子とのパターンに応じて、検査対象情報の各項をノードに変換し、各演算子を各ノードの親子関係に変換し、変換後のグラフ情報をグラフ記憶部に蓄積する翻訳部と、をさらに備えてもよい。このような構成により、検査対象情報をグラフ情報に変換することができる。したがって、人工言語で記述されたケースを、視覚的に理解しやすいグラフ情報で見ることができるようになる。また、本発明による整合性検査装置では、人工言語は、構成的型理論に基づく人工言語であってもよい。このような構成により、その人工言語で記述されたケース自体をプログラムとして実行することもできるようになる。また、本発明による整合性検査装置では、検査部による証明検査によって、エラーのないことが検査された検査対象情報を実行する実行部をさらに備えてもよい。また、本発明による整合性検査装置では、実行部は、検査対象情報を実行することにより、検査対象情報から、整合性の検査対象であるケースの各ノードに応じた項と、各ノードの親子関係に応じた演算子とを陽に記述する形式の検査対象情報を生成してもよい。このような構成により、翻訳の前に、あるいは、翻訳中に、検査対象情報を項や演算子を陽に記述した形式に変換することによって、検査対象情報をグラフ情報に変換することができるようになる。また、本発明による整合性検査装置では、検査対象記憶部では、検査対象情報をグラフ情報に変換する処理に応じた変換プログラムも記憶され、翻訳部は、変換プログラムを実行することによって、検査対象情報をグラフ情報に変換してもよい。このような構成により、その変換プログラムによって、翻訳部による情報の変換が実現されるようになる。また、本発明による整合性検査装置では、検査対象情報と変換プログラムとは、構成的型理論に基づく同じ人工言語で記述されていてもよい。このような構成により、変換プログラム自体についても、証明検査の対象とすることができ、検査済の変換プログラムによって、変換の処理を行うことができるようになる。また、本発明による整合性検査装置では、検査対象情報の項は、メタ変数を含むものであり、人工言語は、対話型証明支援系の人工言語であってもよい。このような構成により、メタ変数を含む検査対象情報例えば、作成途中の検査対象情報であっても、その段階で証明検査を行うことができる。その結果、その段階において、検査対象情報が適切に構成されているかどうかを確認することができる。本発明による整合性検査装置等によれば、アシュランスケースなどの整合性の検査対象であるケースの整合性を、証明検査によって検査することができる。したがって、汎用性の高い方法によって精度よく自動的に検査することができる。以下、本発明による整合性検査装置について、実施の形態を用いて説明する。なお、以下の実施の形態において、同じ符号を付した構成要素及びステップは同一または相当するものであり、再度の説明を省略することがある。実施の形態1本発明の実施の形態1による整合性検査装置について、図面を参照しながら説明する。本実施の形態による整合性検査装置は、人工言語で記述された、整合性の検査対象であるケースに対して、証明検査を行うことによって、そのケースの整合性を検査する。図1は、本実施の形態による整合性検査装置1の構成を示すブロック図である。本実施の形態による整合性検査装置1は、検査対象記憶部11と、検査部12と、検査結果出力部13と、実行部14と、グラフ記憶部15と、翻訳部16と、表示部17と、受付部18とを備える。検査対象記憶部11では、検査対象情報が記憶される。検査対象情報は、整合性の検査対象であるケースを、証明検査の対象となる人工言語により記述した情報である。整合性の検査対象であるケースは、例えば、前述のアシュランスケースやセーフティーケースなどであってもよく、それ以外のケースであってもよい。そのケースは、複数のノードを含む有向非巡回グラフの構造を有するものである。その構造に現れ得る複数のノードの種類には、少なくとも、目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとが含まれる。その複数のノードには、整合性の検査対象であるケースに関する文脈情報に対応するコンテキストノードがさらに含まれてもよい。また、その複数のノードには、証明がまだなされていない未達成ゴールがさらに含まれてもよい。本実施の形態では、整合性の検査対象であるケースが、ゴールノード、ストラテジノード、エビデンスノード、及び、コンテキストノードを有する場合について主に説明する。有向非巡回グラフの構造に含まれる各ノードは、有向非巡回グラフの構造を有するように接続されているため、各ノードは、単数または複数の親ノードを有することになる。但し、非巡回であるため、親の方向、または、子の方向にノードをたどった場合に、元のノードに戻ることはないものとする。その有向非巡回グラフの構造では、ルートノードが単数であってもよく、または、複数であってもよい。本実施の形態の以下の説明では、有向非巡回グラフのルートノードが単数であるとする。なお、ルートノードが単数でない有向非巡回グラフは、通常、ルートノードが単数である複数の有向非巡回グラフに分けて考えることが可能である。ルートノードが複数である有向非巡回グラフは、ルートノードが単数である2以上の有向非巡回グラフの組み合わせであると考えることもできる。また、そのルートノードが単数である有向非巡回グラフは、例えば、木構造であってもよく、または、そうでなくてもよい。木構造である場合には、各ノードは、単数の親ノードを有することになる。本実施の形態では、有向非巡回グラフが木構造である場合について主に説明する。その有向非巡回グラフは、ルートノードであるゴールノードこのゴールノードをトップゴールノードと呼ぶこともあるを、単数または複数の他のゴールノードこのゴールノードをサブゴールノードと呼ぶこともあるに分解し、リーフノードであるエビデンスノードに至るものである。GSNで知られているように、通常、トップゴールノードが複数のサブゴールノードに分解され、それが繰り返されて、最終的に最もリーフ側のサブゴールノードがエビデンスノードによって証明されることになる。したがって、各サブゴールノードが証明されたことになり、その結果、トップゴールノードが証明されたことになる。なお、通常、単数のゴールノードが、複数のゴールノードに分解される際に、ストラテジノードによって分解されることになる。また、エビデンスノードに至るリーフ側の構造が確定されていないゴールノードは、未達成ゴールノードとなる。また、整合性の検査対象であるケース全体の文脈情報、または、そのケースの一部の文脈情報が、コンテキストノードにより示される。検査対象情報は、その複数のノードを含む有向非巡回グラフの構造を有するケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報である。また、その検査対象情報は、前述のように、証明検査の対象となる人工言語により記述された情報である。その人工言語は、証明検査を行うことができる人工言語である。また、その人工言語は、構成的型理論に基づく人工言語であってもよく、または、そうでなくてもよい。本実施の形態では、その人工言語が構成的型理論に基づく人工言語である場合について主に説明する。そのような人工言語として、例えば、AgdaやCoq、NuPRL等が知られている。本実施の形態では、構成的型理論に基づく人工言語がAgdaである場合について主に説明する。また、検査対象情報は、検査対象情報に含まれる各項の定義を含むモデル情報と、検査対象情報に対応する有向非巡回グラフの構造を示す議論構造情報とを有する情報であってもよい。本実施の形態では、主にその場合について説明する。議論構造情報は、整合性の検査対象であるケースにおける各ノードの親子関係を人工言語によって記述した情報である。モデル情報は、例えば、そのモデル情報の全部が議論構造情報に含まれない情報であってもよく、そのモデル情報の全部が議論構造情報に含まれてもよく、または、そのモデル情報の一部が議論構造情報に含まれてもよい。以下、モデル情報のうち、議論構造情報に含まれる情報を局所モデル情報と呼び、議論構造情報に含まれない情報を大局モデル情報と呼ぶこともある。したがって、モデル情報は、そのすべてが大局モデル情報であってもよく、そのすべてが局所モデル情報であってもよく、または、大局モデル情報と局所モデル情報とを含んでいてもよい。また、検査対象情報に含まれる議論構造情報は、具体的な有向非巡回グラフの構造に応じた議論構造情報の生成関数生成プログラムと、引数の値とを含む情報であってもよい。その場合には、議論構造情報そのものによっては、ノードの具体的な親子関係が示されないが、その議論構造情報に含まれる引数の値を、その議論構造情報に含まれる生成関数に適用して、その生成関数を実行することによって、具体的な有向非巡回グラフの構造に応じた議論構造情報が生成されることになるため、実質的に、ノードの具体的な親子関係を示す議論構造情報が与えられた場合と同様であると考えることができる。その具体的な有向非巡回グラフの構造に応じた議論構造情報とは、整合性の検査対象であるケースの各ノードに応じた項と、各ノードの親子関係に応じた演算子とを陽に記述する形式の議論構造情報である。なお、その生成関数の実行は、実行部14によって行われる。また、検査対象情報には、証明検査において用いる情報に関する実行プログラムが含まれていてもよい。その場合には、証明検査が行われる際に、その実行プログラムが実行され、その実行結果を用いて証明検査が行われることになる。その実行結果は、例えば、その時点で得られた情報であってもよく、または、その他の情報であってもよい。具体的には、その実行プログラムが実行されることによって、その時点における値例えば、温度や圧力、センサの値等が取得され、それを用いて証明検査が行われることになってもよい。なお、その実行プログラムの実行は、実行部14によって行われる。ここで、検査対象情報によって記述されるケースの構造について簡単に説明する。図9aで示されるように、一のケースは、ルートノードであるゴールノードと、そのゴールノードの子である部分木構造であるアーギュメントとを有するか、または、ゴールノードをルートノードとする部分ケースと、そのゴールノードを親とするコンテキストノードとを有する。なお、アーギュメントは、図9bで示されるように、ルートノードであるストラテジノードと、そのストラテジノードの子である1以上のケースとを有するか、エビデンスノードそのものであるか、または、ストラテジノードをルートノードとする部分アーギュメントと、そのストラテジノードを親とするコンテキストノードとを有する。なお、子ノードであるケースを有しないストラテジノードは、エビデンスノードと同じであるが、本実施の形態では、そのようなストラテジノードをエビデンスノードとして扱う。整合性の検査対象となるケースは図9で示される構造を有しているため、前述のように、ゴールノードと、ストラテジノードと、エビデンスノードと、コンテキストノードとの親子関係によって記述することができる。なお、図9では、ケースが木構造である場合について説明したが、前述のように、ケースは有向非巡回グラフであってもよい。したがって、その場合には、例えば、エビデンスノードが2以上の親ノードを有してもよい。次に、図9で示されるケースを構成的型理論に基づく人工言語であるAgdaにより記述する場合における検査対象情報について、拡張バッカスナウア記法ExtendedBackus-NaurForm、EBNF;ISO/IEC14977:1996に準じた記法を用いて説明する。ケース、アーギュメント、ゴール、ストラテジ、エビデンス、コンテキストそれぞれのAgda表記の範疇を、Case,Argument,Goal,Strategy,Evidence,Contextと表記するものとする。すると、図9aに対応して、Caseは次のように記述される。Case::=Goal∋Argument|CONTEXT[Context/Case]なお、::=は、左辺の範疇のものは右辺のように構成されることを示すEBNFの記法であり、|は、またはを示す記法である。上の式の場合、一のCaseは、一のGoalgと一のArgumentaからg∋aとして構成されるか、または、一のContextsと一のCasedからCONTEXT[s/d]として構成されるかであることを示している。また、図9bに対応して、Argumentは次のように記述される。Argument::=Strategy{Case}|Evidence|CONTEXT[Context/Argument]ここで、{}は、0以上の繰り返しを示すEBNFの記法である。また、∋、、またはCONTEXT[/]は、演算子である。また、Goal,Strategy,Evidence,Contextは項である。したがって、各ノードの親子関係で示されるケースと、そのケースを人工言語で記述した検査対象情報とは、上述のようにして対応付けられるため、任意のケースを人工言語この場合にはAgdaを用いて記述することができるようになる。また、上述した各演算子の定義について簡単に説明する。まず、∋のAgdaでの定義は次の二行のようになる。_∋_:A:Set→a:A→AA∋a=aしたがって、Agda表記A∋aは、aと同じ値を指し示しつつ、aの型がAであることを明示する表記となる。なお、この演算子∋の定義を言葉で説明すると、第一引数Aが型、第二引数aがA型のときに限り型検査に通り、その場合A型のaを値として返す演算子であると言うことができる。したがって、Agda以外の構成的型理論に基づく人工言語において∋と同様の演算子を定義する際には、そのような性質を有する演算子を定義すればよい。次に、のAgdaでの定義は次の二行のようになる。__:{A:Set}→{B:A→Set}→f:a:A→Ba→a:A→Bafa=faしたがって、Agda表記faは、fa関数fに引数aを適用した結果と同じ値を指し示しつつ、関数部分と引数部分の別を明示する表記となる。なお、この演算子の定義を言葉で説明すると、第一引数fが関数であって、その関数の型をx:A→Bxとして、第二引数aがA型のときに限り型検査に通り、その場合Ba型のfaを値として返す演算子であると言うことができる。したがって、Agda以外の構成的型理論に基づく人工言語においてと同様の演算子を定義する際には、そのような性質を有する演算子を定義すればよい。次に、CONTEXT[s/x]は、ケースxやアーギュメントxに文脈情報文字列sを追加する演算子である。したがって、CONTEXT[s/x]はxである。したがって、Agda以外の構成的型理論に基づく人工言語においてCONTEXT[/]と同様の演算子を定義する際には、そのような性質を有する演算子を定義すればよい。検査対象記憶部11に検査対象情報が記憶される過程は問わない。例えば、記録媒体を介して検査対象情報が検査対象記憶部11で記憶されるようになってもよく、通信回線等を介して送信された検査対象情報が検査対象記憶部11で記憶されるようになってもよく、入力デバイスを介して入力された検査対象情報が検査対象記憶部11で記憶されるようになってもよく、あるいは、翻訳部16がグラフ情報を変換した検査対象情報が検査対象記憶部11で記憶されるようになってもよい。検査対象記憶部11での記憶は、RAM等における一時的な記憶でもよく、あるいは、長期的な記憶でもよい。検査対象記憶部11は、所定の記録媒体例えば、半導体メモリや磁気ディスク、光ディスクなどによって実現されうる。検査部12は、検査対象情報に対して証明検査を行う。この証明検査は、証明検査を行う人工言語においてあらかじめ用意されているものである。この検査部12は、そのような人工言語においてプルーフチェッカーproofcheckerと呼ばれる機能によって実現される。検査部12は、証明検査によって、エラーの有無を取得することができる。また、検査部12は、エラーが存在する場合に、そのエラーの箇所を示す情報をも取得してもよい。エラーの箇所を示す情報は、例えば、検査対象情報における行番号であってもよく、それにコラム番号が加わったものであってもよく、基準となる位置からの文字数やデータ容量例えば、バイト数等であってもよく、または、それらの組み合わせであってもよい。なお、この検査部12の機能は、前述のように、プルーフチェッカーとして公知であり、その詳細な説明を省略する。検査結果出力部13は、検査部12による証明検査の結果を出力する。証明検査の結果は、例えば、エラーの有無を示す情報を含んでいてもよく、エラーが存在する場合に、そのエラーの箇所を示す情報を含んでいてもよく、または、その他の証明検査の結果を含んでいてもよい。証明検査の結果によりエラーの箇所を示す場合には、例えば、行番号やコラム番号等が表示されることによって、エラーの箇所が特定できるようにされてもよく、ハイライト表示例えば、下線や太字等の強調表示がなされたり、他の部分と色が変更されたりしてもよいによってエラーの箇所が示されてもよく、エラーの箇所の先頭にカーソルを移動させることによってエラーの箇所が示されてもよく、あるいは、その他の方法によってエラーの箇所が示されてもよい。ここで、この出力は、例えば、表示デバイス例えば、CRTや液晶ディスプレイなどへの表示でもよく、所定の機器への通信回線を介した送信でもよく、プリンタによる印刷でもよく、スピーカによる音声出力でもよく、記録媒体への蓄積でもよく、他の構成要素への引き渡しでもよい。なお、検査結果出力部13は、出力を行うデバイス例えば、表示デバイスやプリンタなどを含んでもよく、あるいは含まなくてもよい。また、検査結果出力部13は、ハードウェアによって実現されてもよく、あるいは、それらのデバイスを駆動するドライバ等のソフトウェアによって実現されてもよい。実行部14は、検査部12による証明検査によって、エラーのないことが検査された検査対象情報を実行する。その検査対象情報の実行は、例えば、後述する検査対象情報からグラフ情報への変換の際に行われる。検査対象情報からグラフ情報への変換の際に検査対象情報が実行される場合には、実行部14は、前述のように、生成関数と引数の値とを含む議論構造情報において、その引数の値をその生成関数に適用して実行することにより、ノードの具体的な親子関係を示す議論構造情報、すなわち、整合性の検査対象であるケースの各ノードに応じた項と、各ノードの親子関係に応じた演算子とを陽に記述する形式の議論構造情報を生成してもよい。この生成関数の実行は、検査対象情報からグラフ情報への変換の際に行われるものである。その生成関数の実行は、例えば、検査対象情報からグラフ情報への変換の際に、一括して行われてもよく、または、変換の処理の進行に応じて、逐次的に行われてもよい。いずれの場合であっても、実行部14は、ノードの具体的な親子関係を示す議論構造情報を生成するための実行を少なくとも行えばよく、それ以上の実行を行わなくてもよい。なお、実行部14は、検査部12による証明検査の際に検査対象情報を実行してもよい。前述のように、検査対象情報に、証明検査において用いる情報に関する実行プログラムが含まれている場合には、実行部14は、その検査対象情報の証明検査が行われる際に、その実行プログラムを実行し、その実行結果を検査部12に渡してもよい。そして、検査部12において、その実行結果を用いて証明検査が行われることになる。グラフ記憶部15では、グラフ情報が記憶される。グラフ情報は、検査対象情報に対応する有向非巡回グラフの各ノードと、それらの間の親子関係とを示す情報である。また、グラフ情報は、整合性の検査対象であるケースの情報である。前述の検査対象情報は、人工言語で記述されたものであるため、不慣れな者には理解しにくいことがあるが、このグラフ情報は、ノードの親子関係を視覚的に知ることができる情報であるため、専門家でなくても理解しやすい情報である。このグラフ情報は、各ノードの性質を示す情報例えば、各ノードがゴールノードであるのか、ストラテジノードであるのか、エビデンスノードであるのかなどを示す情報と、その各ノードの親子関係を示す情報を含む情報であればよい。したがって、グラフ情報は、例えば、各ノードの情報と、そのノードの親子関係を示すリンク情報とを有する情報であってもよく、親のノードを示す情報を含む各ノードの情報であってもよく、子のノードを示す情報を含む各ノードの情報であってもよい。このように、グラフ情報の構造は問わない。また、グラフ情報は、例えば、XMLのようにマークアップ言語で記述されるものであってもよく、または、その他のデータ形式の情報であってもよい。グラフ記憶部15にグラフ情報が記憶される過程は問わない。例えば、記録媒体を介してグラフ情報がグラフ記憶部15で記憶されるようになってもよく、通信回線等を介して送信されたグラフ情報がグラフ記憶部15で記憶されるようになってもよく、入力デバイスを介して入力されたグラフ情報がグラフ記憶部15で記憶されるようになってもよく、あるいは、翻訳部16が検査対象情報を変換したグラフ情報がグラフ記憶部15で記憶されるようになってもよい。グラフ記憶部15での記憶は、RAM等における一時的な記憶でもよく、あるいは、長期的な記憶でもよい。グラフ記憶部15は、所定の記録媒体例えば、半導体メモリや磁気ディスク、光ディスクなどによって実現されうる。翻訳部16は、検査対象情報と、グラフ情報との間の変換を行う。翻訳部16は、例えば、検査対象情報をグラフ情報に変換し、変換後のグラフ情報をグラフ記憶部15に蓄積してもよく、グラフ情報を検査対象情報に変換し、変換後の検査対象情報を検査対象記憶部11に蓄積してもよく、または、その両方の処理を行ってもよい。本実施の形態では、翻訳部16がその両方の処理を行う場合について主に説明する。検査対象情報をグラフ情報に変換する場合には、翻訳部16は、検査対象情報を、項と演算子とのパターンに応じて、検査対象情報の各項をノードに変換し、各演算子を各ノードの親子関係に変換する。また、グラフ情報を検査対象情報に変換する場合には、翻訳部16は、グラフ情報の各ノードの親子関係のパターンに応じて、グラフ情報の各ノードを項に変換し、各ノードの親子関係を演算子に変換する。なお、翻訳部16による変換の処理の詳細については、フローチャートを用いて後述する。表示部17は、検査対象記憶部11で記憶されている検査対象情報や、グラフ記憶部15で記憶されているグラフ情報を表示する。なお、検査対象情報を表示する際には、表示部17は、その検査対象情報をそのまま表示すればよい。一方、グラフ情報を表示する際には、表示部17は、そのグラフ情報を各ノードの親子関係が分かる有向非巡回グラフの画像を生成して、その画像を表示してもよく、あるいは、グラフ情報をそのまま表示してもよい。なお、ノードと、そのノードの親子関係を示す情報から有向非巡回グラフの画像を生成する方法はすでに公知であり、その詳細な説明を省略する。また、表示部17は、その他の情報を表示してもよい。例えば、実行部14による実行の結果を表示してもよい。なお、表示部17は、それらの表示を行う表示デバイス例えば、CRTや液晶ディスプレイなどを含んでもよく、あるいは含まなくてもよい。また、表示対象の表示は、別の装置においてなされてもよい。その場合には、表示部17は、装置の外部に対して表示対象の情報を送信するものであってもよい。また、表示部17は、ハードウェアによって実現されてもよく、あるいは表示デバイスを駆動するドライバ等のソフトウェアによって実現されてもよい。受付部18は、指示や情報を受け付ける。例えば、受付部18は、検査対象情報に関する受け付けを行い、それに応じて、検査対象記憶部11で記憶されている検査対象情報を変更してもよい。また、例えば、受付部18は、グラフ情報に関する受け付けを行い、それに応じて、グラフ記憶部15で記憶されているグラフ情報を変更してもよい。また、例えば、受付部18は、検査の指示や翻訳の指示を受け付け、それに応じて、検査部12や翻訳部16に対して、検査や翻訳を行う旨の指示を渡してもよい。なお、受付部18が受け付けた情報に応じてグラフ記憶部15で記憶されているグラフ情報を変更し、その変更後のグラフ情報に応じたノードとリンクとを表示部17が表示するシステムとして、D-CaseEditorが知られている。したがって、グラフ情報の変更や、グラフ情報の表示に関する詳細な説明は省略する。そのD-CaseEditorの詳細については、例えば、次のURLを参照されたい。なお、D-CaseのDは、Dependabilityを示す。URL:http://www.il.is.s.u-tokyo.ac.jp/deos/dcase/D-Case_Editor.html受付部18は、例えば、入力デバイス例えば、キーボードやマウス、タッチパネルなどから入力された情報を受け付けてもよく、有線もしくは無線の通信回線を介して送信された情報を受信してもよく、所定の記録媒体例えば、光ディスクや磁気ディスク、半導体メモリなどから読み出された情報を受け付けてもよい。なお、受付部18は、受け付けを行うためのデバイス例えば、モデムやネットワークカードなどを含んでもよく、あるいは含まなくてもよい。また、受付部18は、ハードウェアによって実現されてもよく、あるいは所定のデバイスを駆動するドライバ等のソフトウェアによって実現されてもよい。なお、検査対象記憶部11と、グラフ記憶部15とは、同一の記録媒体によって実現されてもよく、あるいは、別々の記録媒体によって実現されてもよい。前者の場合には、検査対象情報を記憶している領域が検査対象記憶部11となり、グラフ情報を記憶している領域がグラフ記憶部15となる。次に、整合性検査装置1の動作について図2のフローチャートを用いて説明する。ステップS101検査部12は、証明検査を行うかどうか判断する。そして、証明検査を行う場合には、ステップS102に進み、そうでない場合には、ステップS104に進む。なお、検査部12は、例えば、検査の指示が受付部18で受け付けられた場合に、検査を行うと判断してもよく、または、その他のタイミングで検査を行うと判断してもよい。ステップS102検査部12は、検査対象記憶部11で記憶されている検査対象情報について証明検査を行う。そして、その検査結果を取得する。ステップS103検査結果出力部13は、検査部12による検査結果を出力する。そして、ステップS101に戻る。ステップS104受付部18は、検査対象情報に関する情報を受け付けたかどうか判断する。そして、検査対象情報に関する情報を受け付けた場合には、ステップS105に進み、そうでない場合には、ステップS107に進む。ステップS105受付部18は、受け付けた検査対象情報に関する情報に応じて、検査対象記憶部11で記憶されている検査対象情報を変更する。その変更は、例えば、検査対象情報の蓄積であってもよく、検査対象情報の削除であってもよく、検査対象情報の一部の変更であってもよい。ステップS106表示部17は、変更後の検査対象情報を表示する。そして、ステップS101に戻る。ステップS107受付部18は、グラフ情報に関する情報を受け付けたかどうか判断する。そして、グラフ情報に関する情報を受け付けた場合には、ステップS108に進み、そうでない場合には、ステップS110に進む。ステップS108受付部18は、受け付けたグラフ情報に関する情報に応じて、検査対象記憶部11で記憶されているグラフ情報を変更する。その変更は、例えば、グラフ情報の蓄積であってもよく、グラフ情報の削除であってもよく、グラフ情報の一部の変更であってもよい。ステップS109表示部17は、変更後のグラフ情報を表示する。そして、ステップS101に戻る。ステップS110翻訳部16は、検査対象情報をグラフ情報に変換するかどうか判断する。そして、その変換を行う場合には、ステップS111に進み、そうでない場合には、ステップS113に進む。なお、翻訳部16は、例えば、検査対象情報からグラフ情報への変換の指示が受付部18で受け付けられた場合に、その変換を行うと判断してもよく、または、その他のタイミングでその変換を行うと判断してもよい。ステップS111翻訳部16は、検査対象情報をグラフ情報に変換する。その変換の詳細な処理については、図3のフローチャートを用いて後述する。ステップS112表示部17は、変換後のグラフ情報を表示する。そして、ステップS101に戻る。ステップS113翻訳部16は、グラフ情報を検査対象情報に変換するかどうか判断する。そして、その変換を行う場合には、ステップS114に進み、そうでない場合には、ステップS101に戻る。なお、翻訳部16は、例えば、グラフ情報から検査対象情報への変換の指示が受付部18で受け付けられた場合に、その変換を行うと判断してもよく、または、その他のタイミングでその変換を行うと判断してもよい。ステップS114翻訳部16は、グラフ情報を検査対象情報に変換する。その変換の詳細な処理については、図6のフローチャートを用いて後述する。ステップS115表示部17は、変換後の検査対象情報を表示する。そして、ステップS101に戻る。なお、図2のフローチャートにおいて、電源オフや処理終了の割り込みにより処理は終了する。また、図2のフローチャートにおいて、検査対象情報をグラフ情報に変換する際には、検査部12による証明検査によって、問題のないことが確認されているべきである。したがって、ステップS110からステップS111に進む際に、証明検査を行い、問題のないことが確認された場合にのみステップS111に進み、問題がある場合には、ステップS101に戻るようにしてもよい。図3は、図2のフローチャートにおける検査対象からグラフへの翻訳の処理ステップS111の詳細を示すフローチャートである。ステップS201翻訳部16は、検査対象記憶部11で記憶されている検査対象情報において、ケースに応じた記述がなされている箇所を特定する。通常、その箇所は、議論構造情報における有向非巡回グラフに対応する範囲である。その記述の箇所の特定は、例えば、その記述の箇所を図示しない記録媒体に蓄積することであってもよく、その特定した箇所にフラグ等を設定することであってもよく、その特定した箇所を示す情報例えば、行番号やコラム番号等を図示しない記録媒体に蓄積することであってもよく、あるいは、その他の特定であってもよい。ステップS202実行部14は、検査対象情報を実行するかどうか判断する。そして、実行を行う場合には、ステップS203に進み、そうでない場合には、ステップS204に進む。なお、実行部14は、検査対象情報において、ケースが何らかの生成関数を用いて記述されており、項や演算子が陽に記述されていない場合に、検査対象情報を実行すると判断し、そうでない場合に、実行しないと判断してもよい。ステップS203実行部14は、検査対象情報を実行する。すなわち、検査対象情報に含まれる生成関数を実行することによって、項や演算子を陽に記述する形式の検査対象情報を生成する。その実行後の検査対象情報は、検査対象記憶部11に蓄積されてもよい。ステップS204翻訳部16は、ステップS201で特定されたケースに応じた記述の処理、すなわち、そのケースに応じた記述をグラフの情報に変換する処理を行う。この処理の詳細については、図4のフローチャートを用いて後述する。ステップS205翻訳部16は、グラフ記憶部15で記憶されているグラフ情報に、ノード等を追加する処理を行うかどうか判断する。そして、ノード等を追加する処理を行う場合には、ステップS206に進み、そうでない場合には、図2のフローチャートに戻る。なお、翻訳部16は、例えば、検査対象情報にモデル情報が含まれる場合に、ノード等を追加する処理を行うと判断してもよく、議論構造情報にノードの親子関係以外を示す情報が含まれる場合に、ノード等を追加する処理を行うと判断してもよく、あるいは、その他の場合に、ノード等を追加する処理を行うと判断してもよい。ステップS206翻訳部16は、グラフ記憶部15で記憶されているグラフ情報に、ノード等の情報を追加する。そして、図2のフローチャートに戻る。なお、具体的には、翻訳部16は、モデル情報やケース名等に対応したコンテキストノードをグラフ情報に追加してもよく、モデル情報に対応した情報をグラフ情報に追加してもよく、または、その他の情報をグラフ情報に追加してもよい。なお、ノード以外の情報が追加された場合には、グラフ情報が表示される際に、その追加された情報が表示されなくてもよい。すなわち、グラフ情報は、検査対象情報の少なくとも一部の情報を、不可視情報として有してもよい。図3のフローチャートでは、ステップS203において実行部14が生成関数を実行することにより、検査対象情報を一括して項や演算子を陽に記述する形式に変換する場合について説明したが、そうでなくてもよい。例えば、前述のように、翻訳の処理において逐次的にその変換を行ってもよい。また、図3のフローチャートでは、翻訳部16が、検査対象情報をグラフ情報に変換した情報を逐次、グラフ記憶部15に蓄積するものとするが、そうでなくてもよい。翻訳部16は、図示しない記録媒体に順次、グラフ情報の一部の情報を蓄積し、グラフ情報が完成した後に、それをグラフ記憶部15に一括して蓄積してもよい。図4は、図3のフローチャートにおけるケースに応じた記述の処理ステップS204の詳細を示すフローチャートである。ステップS301翻訳部16は、処理の対象となるケースのパターンを特定する。図9aで示されるように、これは通常、ゴールとアーギュメントのパターンか、あるいは、ケースとコンテキストのパターンとなる。このパターンの特定は、あらかじめ図示しない記録媒体で記憶されているパターンを読み出し、そのパターンマッチングにより行うことができる。そのパターンは、例えば、g∋t1や、CONTEXT[s/t2]のパターンである。gは任意のゴールの項であり、t1は任意のアーギュメントであり、t2は任意のケースであり、sは任意のコンテキストの項である。ステップS302翻訳部16は、特定したパターンに応じたノードを生成する。例えば、パターンg∋tを特定した場合には、翻訳部16は、それに応じてgに対応するゴールノードを生成する。また、例えば、パターンCONTEXT[s/t]を特定した場合には、翻訳部16は、それに応じてsに対応するコンテキストノードを生成する。ステップS303翻訳部16は、ステップS302で生成した以外の残りの部分は、ケースであるかどうか判断する。例えば、パターンg∋tを特定した場合には、翻訳部16は、gに対応するゴールノード以外の残りの部分がケースではないアーギュメントtであると判断する。一方、例えば、パターンCONTEXT[s/t]を特定した場合には、翻訳部16は、sに対応するコンテキストノード以外の残りの部分がケースtであると判断する。そして、残りの部分がケースである場合には、ステップS304に進み、そうでない場合には、ステップS305に進む。ステップS304翻訳部16は、その残りの部分について、ケースに応じた記述の処理を実行する。その処理は、図4のフローチャートで示されるものである。すなわち、翻訳部16は、ケースに応じた記述の処理を再帰的に実行することになる。ステップS305翻訳部16は、その残りの部分について、アーギュメントに応じた記述の処理を実行する。その処理の詳細については、図5のフローチャートを用いて後述する。ステップS306翻訳部16は、ステップS302で生成したノードと、その残りの部分とのリンクを生成する。そのリンクの向きは、ステップS301で特定したパターンに応じたものとなる。そして、上位のフローチャートに戻る。例えば、パターンg∋tを特定した場合には、翻訳部16は、gに対応するゴールノードが親となり、tに対応するアーギュメントのルートノードが子となるリンクを生成する。また、例えば、パターンCONTEXT[s/t]を特定した場合には、翻訳部16は、sに対応するコンテキストノードが子となり、残りのケースtのルートノードゴールノードが親となるリンクを生成する。図5は、図4のフローチャートにおけるアーギュメントに応じた記述の処理ステップS305の詳細を示すフローチャートである。ステップS401翻訳部16は、処理の対象となるアーギュメントのパターンを特定する。図9bで示されるように、これは通常、ストラテジとケースのパターンか、エビデンスのパターンか、あるいは、アーギュメントとコンテキストのパターンとなる。このパターンの特定は、あらかじめ図示しない記録媒体で記憶されているパターンを読み出し、そのパターンマッチングにより行うことができる。そのパターンは、例えば、ft1t2...tnや、CONTEXT[s/t]のパターンである。前者のパターンで、nが1以上の場合には、fは、任意のストラテジの項であり、t1等は、任意のケースに応じた項であり、nが0の場合には、fは、任意のエビデンスの項である。また、後者のパターンの場合、tは、任意のアーギュメントの項であり、sは、任意のコンテキストの項である。ステップS402翻訳部16は、特定したパターンに応じたノードを生成する。例えば、n≧1のパターンft1t2...tnを特定した場合には、翻訳部16は、それに応じてfに対応するストラテジノードを生成する。また、例えば、n=0のパターンft1t2...tnを特定した場合には、翻訳部16は、それに応じてfに対応するエビデンスノードを生成する。また、例えば、パターンCONTEXT[s/t]を特定した場合には、翻訳部16は、それに応じてsに対応するコンテキストノードを生成する。ステップS403翻訳部16は、生成したノードがリーフノード、すなわち、エビデンスノードであるかどうか判断する。そして、リーフノードである場合には、上位のフローチャートに戻り、そうでない場合には、ステップS404に進む。ステップS404翻訳部16は、ステップS403で生成した以外の残りの部分は、ケースであるかどうか判断する。例えば、n≧1のパターンft1t2...tnを特定した場合には、翻訳部16は、fに対応するストラテジノード以外の残りの部分がケースt1、t2、...、tnであると判断する。また、例えば、パターンCONTEXT[s/t]を特定した場合には、翻訳部16は、sに対応するコンテキストノード以外の残りの部分がアーギュメントtであると判断する。そして、残りの部分がケースである場合には、ステップS405に進み、そうでない場合には、ステップS408に進む。ステップS405翻訳部16は、その残りの部分について、ケースに応じた記述の処理を実行する。その処理は、図4のフローチャートで示されるものである。ステップS406翻訳部16は、ステップS402で生成したノードと、その残りの部分とのリンクを生成する。そのリンクの向きは、ステップS401で特定したパターンに応じたものとなる。そして、上位のフローチャートに戻る。例えば、n≧1のパターンft1t2...tnを特定した場合には、翻訳部16は、fに対応するストラテジノードが親となり、ステップS405で処理を行ったケースのルートノードゴールノードが子となるリンクを生成する。ステップS407翻訳部16は、まだ処理のなされていないケースが存在するかどうか判断する。そして、存在する場合には、ステップS405に戻って、そのケースに応じた記述の処理を実行し、そうでない場合には、上位のフローチャートに戻る。なお、ステップS401において、n≧1のパターンft1t2...tnが特定された場合には、ステップS405,S406の処理がn回、繰り返されることになる。ステップS408翻訳部16は、その残りの部分について、アーギュメントに応じた記述の処理を実行する。その処理は、図5のフローチャートで示されるものである。すなわち、翻訳部16は、アーギュメントに応じた記述の処理を再帰的に実行することになる。ステップS409翻訳部16は、ステップS402で生成したノードと、その残りの部分とのリンクを生成する。そのリンクの向きは、ステップS401で特定したパターンに応じたものとなる。そして、上位のフローチャートに戻る。例えば、パターンCONTEXT[s/t]を特定した場合には、翻訳部16は、sに対応するコンテキストノードが子となり、残りのアーギュメントtのルートノードストラテジノード、または、エビデンスノードが親となるリンクを生成する。図6は、図2のフローチャートにおけるグラフから検査対象への翻訳の処理ステップS114の詳細を示すフローチャートである。ステップS501翻訳部16は、グラフ記憶部15で記憶されているグラフ情報において、ルートノードを特定する。本実施の形態では、ルートノードが1個である有向非巡回グラフを扱うため、このルートノードは1個に特定される。なお、ルートノードは、親ノードを有さないノードである。したがって、グラフ情報に含まれるノードやリンクを示す情報を用いて、各ノードに親ノードが存在するかどうか判断し、親ノードが存在しないと判断されたノードがルートノードとなる。なお、ルートノードの特定は、例えば、そのルートノードを識別する情報を図示しない記録媒体に蓄積することであってもよく、そのルートノードに対応付けてフラグ等を設定することであってもよく、あるいは、その他の特定であってもよい。ステップS502翻訳部16は、ステップS501で特定したノードをルートノードとするケースに関する処理を行う。この処理の詳細については、図7のフローチャートを用いて後述する。ステップS503翻訳部16は、検査対象情報に追加する情報が存在するかどうか判断する。そして、存在する場合には、ステップS504に進み、そうでない場合には、図2のフローチャートに戻る。ステップS504翻訳部16は、グラフ情報に含まれる情報を検査対象情報に追加する。例えば、グラフ情報に不可視情報が含まれる場合には、その不可視情報に対応するモデル情報を検査対象情報に追加してもよい。また、グラフ情報に、例えば、モデル情報やケース名等に対応したコンテキストノードが含まれる場合には、そのコンテキストノードに含まれるモデル情報やケース名等を検査対象情報に追加してもよい。そして、図2のフローチャートに戻る。図6のフローチャートでは、翻訳部16が、グラフ情報を検査対象情報に変換した情報を逐次、検査対象記憶部11に蓄積するものとするが、そうでなくてもよい。翻訳部16は、図示しない記録媒体に順次、検査対象情報の一部の情報を蓄積し、検査対象情報が完成した後に、それを検査対象記憶部11に一括して蓄積してもよい。また、グラフ情報を検査対象情報に翻訳する際には、グラフ情報においてモデル情報に対応する情報が含まれていないこともあり得る。そのような場合には、グラフ情報を、検査対象情報の議論構造情報に対応する部分に翻訳し、その後、検査対象情報において、適宜、モデル情報に対応する情報が追加されてもよい。図7は、図6のフローチャートにおけるケースの処理ステップS502の詳細を示すフローチャートである。ステップS601翻訳部16は、カウンタiを1に設定する。ステップS602翻訳部16は、処理対象となっているケースのルートノードを親とするi番目のリンクについて、親子関係のパターンを特定する。図9aで示されるように、これは通常、親のゴールノードと、子のアーギュメントとのパターンか、親のゴールノードと、子のコンテキストノードとのパターンとなる。なお、子がアーギュメントである場合には、具体的には、子のルートノードは、ストラテジノードかエビデンスノードとなる。このパターンの特定は、あらかじめ図示しない記録媒体で記憶されているパターンを読み出し、そのパターンマッチングにより行うことができる。そのパターンは、例えば、親ノード、子ノードが、ゴールノード、ストラテジノードであるパターンや、ゴールノード、エビデンスノードであるパターン、または、ゴールノード、コンテキストノードであるパターンである。ステップS603翻訳部16は、i番目のリンクのリンク先がアーギュメントであるかどうか判断する。例えば、ステップS602でパターンゴールノード、ストラテジノードや、ゴールノード、エビデンスノードを特定した場合には、翻訳部16は、リンク先がアーギュメントであると判断し、ステップS602でパターンゴールノード、コンテキストノードを特定した場合には、翻訳部16は、リンク先がコンテキストノードである、すなわち、アーギュメントでないと判断する。そして、リンク先がアーギュメントである場合には、ステップS604に進み、そうでない場合には、ステップS605に進む。ステップS604翻訳部16は、i番目のリンクのリンク先のノードがルートノードであるアーギュメントに関する処理を行う。この処理の詳細については、図8のフローチャートを用いて後述する。ステップS605翻訳部16は、i番目のリンクのリンク先であるコンテキストノードに対応する項を生成する。その項は、演算子CONTEXT[s/]のsに対応する項である。ステップS606翻訳部16は、i番目のリンクについて特定したパターンに応じた演算子を生成する。例えば、パターンゴールノード、ストラテジノードや、ゴールノード、エビデンスノードを特定した場合には、翻訳部16は、ゴールノードの項∋ストラテジノードをルートノードとするアーギュメントの項や、ゴールノードの項∋エビデンスノードをルートノードとするアーギュメントの項となる演算子∋を生成する。また、例えば、パターンゴールノード、コンテキストノードを特定した場合には、翻訳部16は、CONTEXT[コンテキストノードの項/ゴールノードをルートノードとするケースの項]となる演算子CONTEXT[/]を生成する。ステップS607翻訳部16は、カウンタiを1だけインクリメントする。ステップS608翻訳部16は、処理対象となっているケースのルートノードを親とするi番目のリンクが存在するかどうか判断する。そして、存在する場合には、ステップS602に戻り、存在しない場合には、ステップS609に進む。ステップS609翻訳部16は、処理対象となっているケースのルートノードであるゴールノードの項を生成する。ステップS610翻訳部16は、i-1個のリンクのうち、リンク先にアーギュメントを持つものが一つだけあり、他は全てリンク先にコンテキスト等の他のノードを持つかどうか判断する。そして、そうである場合には、ステップS611に進み、そうでない場合には、ステップS612に進む。ステップS611翻訳部16は、ステップS604~S606,S609で生成したアーギュメントの項やリンク先の項、演算子、ルートノードであるゴールノードの項を用いて、処理の対象となっているケースの項を生成する。例えば、非アーギュメントの子が全てコンテキストノードである場合に、翻訳部16は、ゴールノードをルートノードにもつケースの項として、CONTEXT[コンテキストノードの項1/CONTEXT[コンテキストノードの項2/...CONTEXT[コンテキストノードの項{i-2}/ゴールノードの項∋アーギュメントの項]...]]を生成する。なお、ここでi≧2であり、i=2の場合には、演算子CONTEXT[/]は用いられない。非アーギュメントの子にコンテキストノード以外のものがある場合も、上のCONTEXT[/]に代えてステップS606で生成される演算子を用いて、同様にケースの項を生成する。そして、上位フローチャートに戻る。ステップS612翻訳部16は、ケースの構造に合わないグラフが処理されたことを表すエラーケースの項を生成する。エラーケースの項としては、証明検査の結果が必ずエラーになるものを選ぶ。また、エラーケースの項は、エラーを生じたケースのルートノードを指定する情報を参考に含んでいてもよく、それぞれの子の翻訳結果である項を参考に含んでいてもよい。そして、上位フローチャートに戻る。なお、ステップS612において、翻訳部16は、ケースの構造に合わないグラフが処理されたことの警告を出力してもよく、また、上位のフローチャートの処理を含めてステップS114を異常終了してもよい。図8は、図7のフローチャートにおけるアーギュメントの処理ステップS604の詳細を示すフローチャートである。ステップS701翻訳部16は、処理対象となっているアーギュメントのルートノードにリンク先のノードが存在するかどうか判断する。そして、リンク先のノードが存在する場合には、ステップS702に進み、そうでない場合には、ステップS710に進む。ステップS702翻訳部16は、カウンタjを1に設定する。ステップS703翻訳部16は、処理対象となっているアーギュメントのルートノードを親とするj番目のリンクについて、親子関係のパターンを特定する。図9bで示されるように、これは通常、親のストラテジノードと、子のケースとのパターンか、親のストラテジノードと、子のコンテキストノードとのパターンが、親のエビデンスノードと子のコンテキストノードのパターンとなる。なお、子がケースである場合には、具体的には、子のルートノードはゴールノードとなる。このパターンの特定は、あらかじめ図示しない記録媒体で記憶されているパターンを読み出し、そのパターンマッチングにより行うことができる。そのパターンは、例えば、親ノード、子ノードが、ストラテジノード、ゴールノードであるパターンや、ストラテジノード、コンテキストノードであるパターン、または、エビデンスノード、コンテキストノードであるパターンである。ステップS704翻訳部16は、j番目のリンクのリンク先がケースであるかどうか判断する。例えば、ステップS703でパターンストラテジノード、ゴールノードを特定した場合には、翻訳部16は、リンク先がケースであると判断し、ステップS703でパターンストラテジノード、コンテキストノードを特定した場合には、翻訳部16は、リンク先がコンテキストノードである、すなわち、ケースでないと判断する。そして、リンク先がケースである場合には、ステップS705に進み、そうでない場合には、ステップS706に進む。ステップS705翻訳部16は、j番目のリンクのリンク先であるゴールノードがルートノードであるケースに関する処理を行う。その処理は、図7のフローチャートで示されるものである。ステップS706翻訳部16は、j番目のリンクのリンク先が、例えば、コンテキストノードであった場合には、コンテキストノードに対応する項を生成する。その項は、演算子CONTEXT[s/]のsに対応する項である。ステップS707翻訳部16は、j番目のリンクについて特定したパターンに応じた演算子を生成する。例えば、パターンストラテジノード、ゴールノードを特定した場合には、翻訳部16は、ストラテジノードの項ゴールノードをルートノードとするケースの項となる演算子を生成する。また、例えば、パターンストラテジノード、コンテキストノードを特定した場合には、翻訳部16は、CONTEXT[コンテキストノードの項/ストラテジノードをルートノードとするアーギュメントの項]となる演算子CONTEXT[/]を生成する。ステップS708翻訳部16は、カウンタjを1だけインクリメントする。ステップS709翻訳部16は、処理対象となっているアーギュメントのルートノードを親とするj番目のリンクが存在するかどうか判断する。そして、存在する場合には、ステップS703に戻り、存在しない場合には、ステップS710に進む。ステップS710翻訳部16は、処理対象となっているアーギュメントのルートノードに応じた項を生成する。例えば、処理対象となっているアーギュメントがエビデンスノードである場合には、エビデンスの項を生成し、処理対象となっているアーギュメントのルートノードがストラテジノードである場合には、そのストラテジノードの項を生成する。ステップS711翻訳部16は、ステップS705~S707,S710で生成したケースの項やリンク先の項、演算子、ルートノードの項を用いて、処理の対象となっているアーギュメントの項を生成する。すなわち、翻訳部16は、処理対象となっているアーギュメントのルートノードにリンクがなかった場合、すなわち、ステップS701からステップS710に進んだ場合には、ステップS710で生成した項そのものをアーギュメントの項とする。一方、処理対象となっているアーギュメントのルートノードにリンクがあった場合には、例えば、翻訳部16は、さらに、ケースでない子が全てコンテキストノードであったときに、ステップS705で生成されたケースの項をケース項1、ケース項2、...、ケース項k、ステップS706で生成されたコンテキストノードの項をコンテキストノード項1、コンテキストノード項2、...、コンテキストノード項mとおきここで、k、m≧0、j-1=kmとなる、処理対象となっているアーギュメントの項として、CONTEXT[コンテキストノード項1/CONTEXT[コンテキストノード項2/...CONTEXT[コンテキストノード項m/ステップS710で生成されたストラテジまたはエビデンスの項ケース項1ケース項2...ケース項k]...]]を生成する。非ケースの子にコンテキストノード以外のものがある場合も、上のCONTEXT[/]に代えてステップS707で生成される演算子を用いて、同様にアーギュメントの項を生成する。そして、上位のフローチャートに戻る。なお、アーギュメントのルートノードがエビデンスノードであり、かつk>0である場合には、ステップS612と同様にアーギュメントの構造に合わないグラフが処理されたことを表すエラーアーギュメントの項を生成してもよく、または、上位のフローチャートの処理を含めてステップS114を異常終了してもよい。また、図3~図8のフローチャートを用いて説明した翻訳の処理は一例であり、それ以外の処理によって、検査対象情報をグラフ情報に翻訳してもよく、または、グラフ情報を検査対象情報に翻訳してもよい。また、図3~図8のフローチャートにおける翻訳の処理は、ケースが木構造を有する場合の処理である。ケースが有向非巡回グラフの構造を有する場合の処理については後述する。次に、本実施の形態による整合性検査装置1の動作について、具体例を用いて説明する。この具体例では、構成的型理論に基づく人工言語がAgdaであり、整合性の検査対象がディーケースである場合について説明する。ディーケースは、前述のケースの概念を一部拡張した具体例である。また、この具体例では、整合性の検査対象であるディーケースが、木構造を有する場合について説明する。なお、ディーケース概念の本来の表記はD-Caseであるが、前述のCaseの具体例として次に定義するD-Caseとの混乱をさけるため、ここではカナで表記する。また、この具体例における記述についてさらに詳細に説明する。D-Case前述のCase,Argument,Goal,Strategy,Evidenceは、次のようになる。D-Case::=Goal∋Argument|CONTEXT[Context/D-Case]Argument::=Strategy{D-Case}|Evidence|CONTEXT[Context/Argument]Goal::=FormalGoal|<<FormalGoal/Description>>Strategy::=FormalStrategy|<FormalStrategy/Description>Evidence::=FormalEvidence|<FormalEvidence/Description>なお、Contextは、Descriptionである。また、FormalStrategy,FormalEvidenceはAgda項Agda言語での式である。また、FormalGoalは、Set型のAgda項であり、Descriptionは、String型のAgda項である。このように、Descriptionを記述できることによって、検査対象情報をディーケースのグラフ情報に翻訳した際に、そのDescriptionの文字列をノードに対応付けて表示することも可能である。この具体例での検査対象情報は、D-Caseに名称をつける定義を含むことができる。さらに、この定義は、パラメータを含むことができる。定義されたD-Caseをその名称で参照できることの効用については、後述する。この具体例では、D-Caseの定義を、Agda言語における関数定義の宣言によって行う。後者の一般的な記述は、次のようになる。FunctionDefinition::=[TypeSignature]FunctionClause{FunctionClause}{Pragma}TypeSignature::=FunctionName:AgdaTypeFunctionClause::=LeftHandSide=RightHandSideLeftHandSide::=FunctionName{Pattern}Pattern::=PatternVariable|ConstructorName{Pattern}ここで、[]は、オプションであることを示すEBNFの表記である。また、AgdaTypeはSet型のAgda項であり、PatternVariableは、Agdaの識別子であり、ConstructorNameは、Agdaのコンストラクター識別子であり、RightHandSideは、Agdaの表現である。FunctionDefinitionは、TypeSignatureと、1以上のFunctionClauseと、0個以上のPragmaプラグマとから構成される。TypeSignatureは、関数名と、その型とを規定する。FunctionClauseから型を推測できるのであれば、そのTypeSignatureは省略してもよい。また、FunctionClauseは、左辺LeftHandSideと右辺RightHandSideとを等号でつなぐものである。左辺は、0以上のPatternの適用された関数名である。Patternは、PatternVariable変数であるか、あるいは、0以上のサブPatternに適用されたコンストラクター識別子である。右辺は、左辺に現れたPatternVariableの使用されたAgda項である。Pragmaは、関数定義宣言を処理するAgda言語処理系に対する指令であり、定義されるところの関数に特定の情報を付帯させるものである。この具体例では、整合性の検査対象の概念も、ディーケースの定義を含むよう拡張される。概念自体は、人工言語Agdaで検査対象情報として記述される以前の情報であるが、含まれるべき情報の構成要素を便宜上EBNF記法で表すと次のようになる。ディーケース宣言::=SingleClauseDeclSingleClauseDecl::=SingleClauseSignatureディーケースSingleClauseSignature::=DCaseName{Pattern}{PatternVariableDecl}PatternVariableDecl::=PatternVariableAgdaTypeSingleClauseSignatureは、定義されるところのD-Caseの名前D-CaseNameと、それがとり得る0個以上の引数のPatternと、そのPattern中の各PatternVariableとその型の情報をもつ0個以上のPatternVariableDeclとから構成される。SingleClauseDeclは、SingleClauseSignatureと、その中の各PatternVariableをパラメータとして含むディーケースから構成される。これは、上述の説明における関数定義で、FunctionClauseをひとつだけ持つFunctionDefinitionに相当する。なお、PatternVariableの型は、AgdaTypeでなくともそれに変換可能なものであってもよいが、この具体例では簡単のためAgdaTypeとしている。また、この具体例では、ディーケース宣言を議論構造情報に対応する有向非巡回グラフとして表す場合には、ディーケース宣言中のディーケースのグラフのルートノードの子ノードとして、SingleClauseSignatureに含まれるDCaseName{Pattern}{PatternVariableDecl}の情報を有するコンテキストノードを生成するものとする。そのコンテキストノードにおいて、DCaseName{Pattern}は、Clauseとしてコンテキストに含められ、各パラメータと、その型とを示す{PattenVariableDecl}は、Parametersとしてコンテキストに含められるものとする。次に、Agdaで記述された検査対象情報において、ケースに応じた記述の特定の処理ステップS201について簡単に説明する。まず、この具体例では、関数FunctionNameの関数定義に、それがケースに応じた記述を含むという情報を付加するPragma{-DCASEFunctionNameroot-}を導入する。翻訳部16は、検査対象情報において、このようなPragmaをもつFunctionDefinitionを見つける。ここでは、そのようなFunctionDefinitionが、一だけFunctionClauseを持つ場合について説明する。このFunctionClauseのRightHandSideであるところのAgda項が、D-Caseとして特定される。これがステップS201でいうケースに応じた記述となるため、それについて図3のフローチャートにおけるステップS202以降の処理が実行されることになる。その結果として、このD-Caseに対応するディーケースのグラフグラフ情報を得る。また、この具体例では、翻訳部16は、一のそのようなFunctionDefinition全体を、一のディーケース宣言SingleClauseDeclのグラフに変換するように拡張されている。具体的には、翻訳部16は、LeftHandSideのFunctionNameをSingleClauseSignatureのDCaseNameとし、LeftHandSideの{Pattern}をSingleClauseSignatureの{Pattern}とし、LeftHandSideとTypeSignatureから、Agdaプルーフチェッカーの機能を用いて、SingleClauseSignatureの{PatternVariableDecl}を推測して生成して、SingleClauseSignatureを構成する。翻訳部16は、これを上述の説明のようなコンテキストノードとし、RightHandSideであるところのAgda項に対応するグラフのルートノードに子として追加する。次に、この具体例における一の特定のD-Caseに基づいて詳細を説明する。ユーザは、キーボードを操作することにより、図10で示される検査対象情報200を入力し、その検査対象情報200が受付部18で受け付けられ、検査対象記憶部11に蓄積され、表示部17によって表示されたとするステップS104~S106。図10において、検査対象情報200には、モデル情報201と、議論構造情報202とが含まれている。モデル情報201において、TopGoal,SubGoal-A,SubGoal-Bは、Set型を有していること、つまり、各々それ自体が型であることが宣言されている。Agda言語は命題を型として扱うため、この宣言は、各々をゴールとして宣言することになる。また、topStrategyは、SubGoal-A型のデータをもらい、SubGoal-B型のデータをもらい、TopGoal型のデータを返す関数の型を有していることが宣言されている。また、Evidence-Aは、SubGoal-A型を有し、Evidence-Bは、SubGoal-B型を有していることが宣言されている。また、議論構造情報202では、図11で示される木構造のディーケースのグラフ情報がAgdaによって記述されている。なお、この図10で示される検査対象情報200は、エラーの存在しないものである。したがって、ユーザが、検査対象情報について証明検査をする旨の指示を入力し、それに応じて検査部12が証明検査を行ったとしてもステップS101,S102、エラーは検出されないことになるステップS103。なお、例えば、議論構造情報202において、Evidence-Aを、Evidence-Bに書き間違えていたとする。そのような検査対象情報200について証明検査を行った場合にはステップS101,S102、議論構造情報202のSubGoal-A∋Evidence-BにおけるEvidence-Bがエラーであることが検知され、そのEvidence-Bの箇所がハイライト表示されることになるステップS103。そのハイライト表示は,例えば、その箇所を赤字で表示することであってもよい。なお、ハイライト表示されていない文字は、赤字以外で表示されているものとする。ユーザは、そのハイライト表示されたEvidence-Bを見ることによって、そこにエラーの存在することを容易に把握することができ、そのEvidence-BをEvidence-Aに書き換えることによって、エラーを解消することができるステップS104~S106。次に、検査対象情報200をグラフ情報に翻訳する処理について説明する。この具体例で用いるグラフ情報のデータ形式は、上述の説明で参照したD-CaseEditorの用いるXML形式に準じる。図10で示される検査対象情報200が検査対象記憶部11で記憶されている状態において、ユーザが、検査対象情報をグラフ情報に翻訳する旨の指示を整合性検査装置1に入力したとする。すると、その指示は受付部18で受け付けられ、翻訳部16に渡される。そして、翻訳部16は、検査対象情報をグラフ情報に翻訳するタイミングであると判断しステップS110、検査対象情報をグラフ情報に翻訳する処理を行うステップS111。具体的には、翻訳部16は、検査対象情報200において、Pragma{-DCASEmy-D-Caseroot-}を特定し、関数名FunctionNamemy-D-Caseを取得する。また、翻訳部16は、その関数名を用いて、LeftHandSideであるmy-D-Caseを特定し、それと等号で関係付けられているRightHandSideであるD-Caseを特定するステップS201。すなわち、特定されたD-Caseは、TopGoal∋topStrategySubGoal-A∋Evidence-ASubGoal-B∋Evidence-Bである。その後、翻訳部16は、図示しない経路を介して実行部14に対して、検査対象情報200を実行するかどうか判断するように指示する。すると、実行部14は、検査対象記憶部11で記憶されている検査対象情報200を参照し、議論構造情報202において、プログラムで記載されている箇所は存在しないため、実行する必要がないと判断しステップS202、その結果を図示しない経路を介して翻訳部16に渡す。その判断結果を受け取ると、翻訳部16は、上記のD-Caseに対してケースに応じた記述の処理ステップS204を行う。具体的には、翻訳部16は、パターンマッチングにより、g∋tのパターンを特定しステップS301、そのパターンのgに対応するゴールノードを生成するステップS302。すなわち、翻訳部16は、図12Aで示されるグラフ情報300におけるTopGoalに対応するノードの情報301を生成する。ノードの情報301において、type=Goalは、そのノードがゴールノードであることを示している。ストラテジノードの場合には、type=Strategyとなり、エビデンスノードの場合には、type=Evidenceとなり、コンテキストノードの場合には、type=Context1となるなお、Contextではなく、Context1となる理由については後述する。id=001は、ノードの識別子であり、ノードの生成時に、各ノードを識別できるように付与されるものである。この具体例では、各ノードの情報を生成するごとに、idが1ずつインクリメントされるものとする。name=G1は、グラフ情報の表示の際に表示されるノードの名称である。このノードの名称も、ノードの生成時に適宜、生成されるものである。この具体例では、typeの先頭の文字と数字とを組み合わせ、重複しないように生成される。value=TopGoalは、検査対象情報200における項の値である。なお、タグ<dcase:description>と、タグ</dcase:description>との間には何も情報が含まれていないが、ゴールの項が<<FormalGoal/Description>>のように記述されていた場合には、そのDescription記述が、両タグの間に含められることになる。他のノードの情報を生成する際にも、翻訳部16は、typeやid、nameを生成し、検査対象情報200からDescriptionや項の値を読み出すことによって、そのノードの情報を生成するものとする。次に、翻訳部16は、残りがケースであるかどうか判断する。この場合には、ステップS301において、g∋tのパターンが特定されたため、残りはアーギュメントであるため、翻訳部16は、残りはケースではないと判断して、アーギュメントに応じた記述の処理を行うステップS303,S305。具体的には、翻訳部16は、残りの部分であるtopStrategySubGoal-A∋Evidence-ASubGoal-B∋Evidence-Bについて、パターンマッチングにより、ft1t2のパターンを特定しステップS401、n=2であるため、そのパターンのfに対応するストラテジノードを生成するステップS402。すなわち、翻訳部16は、図12Aで示されるグラフ情報300におけるtopStrategyに対応するノードの情報302を生成する。そのノードの情報302の生成方法は、前述したノードの情報301の生成方法と同様である。その後、翻訳部16は、ステップS401においてパターンft1t2が特定されたため、生成したノードはリーフではなく、残りはケースであると判断しステップS403,S404、まずt1であるSubGoal-A∋Evidence-Aについて、ケースに応じた記述の処理を行うステップS405。具体的には、翻訳部16は、パターンマッチングにより、g∋tのパターンを特定しステップS301、そのパターンのgに対応するゴールノードを生成するステップS302。すなわち、翻訳部16は、グラフ情報300におけるSubGoal-Aに対応するノードの情報303を生成する。そして、翻訳部16は、残りがアーギュメントであると判断し、そのアーギュメントに応じた記述の処理を行うステップS303,S304。具体的には、翻訳部16は、残りの部分であるEvidence-Aについて、パターンマッチングにより、fのパターンを特定しステップS401、n=0であるため、そのパターンのfに対応するエビデンスノードを生成するステップS402。すなわち、翻訳部16は、グラフ情報300におけるEvidence-Aに対応するノードの情報304を生成する。その後、翻訳部16は、エビデンスノードを生成したため、リーフであると判断しステップS403、ゴールノードSubGoal-Aから、エビデンスノードEvidence-Aへのリンクを生成するステップS306。すなわち、翻訳部16は、図12Bで示されるグラフ情報300におけるSubGoal-AからEvidence-Aまでのリンクの情報311を生成する。リンクの情報311において、source=003は、リンク元のノード、すなわち、SubGoal-Aのノードの識別子である。また、target=004は、リンク先のノード、すなわち、Evidence-Aのノードの識別子である。id=Link-003-004は、リンクの識別子であり、各リンクを識別できるように、リンクの生成時に、リンク元のノードの識別子とリンク先のノードの識別子とを用いて生成される。name=Link-003-004は、リンクの名称であり、この具体例では、リンクの識別子と同じである。他のリンクの情報を生成する際にも、翻訳部16は、リンク元の識別子とリンク先の識別子とを用いて、sourceやtarget、id等を生成するものとする。その後、t1に対応するケースに応じた記述の処理が終了したため、翻訳部16は、そのケースと、topStragegyに対応するストラテジノードとの間のリンクを生成するステップS406。すなわち、翻訳部16は、図12Bで示されるグラフ情報300におけるtopStragegyから、t1のルートであるSubGoal-Aまでのリンクに応じたリンクの情報312を生成する。その後、翻訳部16は、未処理のケースt2があるためステップS407、そのt2であるSubGoal-B∋Evidence-Bについて、t1の場合と同様に、ケースに応じた記述の処理を行うステップS405。具体的には、翻訳部16は、g∋tのパターンを特定しステップS301、そのパターンのgに対応するゴールノードに応じたノードの情報305を生成するステップS302。そして、翻訳部16は、残りがアーギュメントであると判断し、そのアーギュメントに応じた記述の処理を行うステップS303,S304。具体的には、翻訳部16は、残りの部分であるEvidence-Bについて、fのパターンを特定しステップS401、そのパターンのfに対応するエビデンスノードに応じたノードの情報306を生成するステップS402。その後、翻訳部16は、エビデンスノードを生成したため、リーフであると判断しステップS403、ゴールノードSubGoal-Bから、エビデンスノードEvidence-Bへのリンクに応じたリンクの情報313を生成するステップS306。そして、t2に対応するケースに応じた記述の処理が終了したため、翻訳部16は、topStragegyから、t2のルートであるSubGoal-Bまでのリンクに応じたリンクの情報314を生成するステップS406。これらの処理によって、topStragegy以下の各ノードや各リンクを生成する処理が終了したため、翻訳部16は、ゴールノードTopGoalからアーギュメントのルートであるストラテジノードtopStragegyまでのリンクに応じたリンクの情報315を生成するステップS306。その後、翻訳部16は、検査対象情報200にモデル情報やD-Caseの名称が存在するため、そのモデル情報201に応じたタグや、D-Caseの名称に応じたコンテキストノードを追加すると判断しステップS205、LeftHandSideに対応するmy-D-Caseを含むコンテキストノードに応じたノードの情報307と、D-CaseのルートであるTopGoalのゴールノードから、そのコンテキストノードまでのリンクに応じたリンクの情報316とを生成する。なお、そのコンテキストノードの情報307において、演算子CONTEXT[/]から生成されたコンテキストノードと区別するため、type=context2としている。なお、演算子CONTEXT[/]から生成されたコンテキストノードから生成されたコンテキストノードでは、type=context1になるものとする。また、そのコンテキストノードでは、そのLeftHandSideの情報ここでは、D-Caseの名称がvalueではなく、descriptionに含められるものとする。さらに、翻訳部16は、グラフ情報300において、モデル情報201に応じたプロパティーの情報321を生成するステップS206。このようにして、グラフ情報300が生成されることになる。なお、プロパティーの情報321において、xD;xA;は、改行の文字コードであり、8594;は右矢印→の文字コードである。また、グラフ情報300の先頭と後端のD-Caseに関するタグや、ノードやリンクの情報の前後に記載されているタグ等は、グラフ情報300を生成するはじめの時点において生成されてもよく、あるいは、ノードやリンク、プロパティー等のタグが生成された後に生成されてもよい。その後、表示部17は、グラフ記憶部15で記憶されているグラフ情報300を読み出し、各ノードの親子関係を取得して、各ノードの親子関係を示す図11の画像を表示するステップS112。図11において、type=Goalであるノード211,214,216は、矩形で表示され、type=Strategyであるノード213は、平行四辺形で表示され、type=Evidenceであるノード215,217は、楕円で表示され、type=ContextNNは1以上の整数であるノード212は、角丸四角形で表示される。それらの図形は、図示しない記録媒体において記憶されており、表示部17は、それらの図形を適宜、読み出すことによって、各ノードに応じた図形を表示してもよい。また、表示部17は、その図形中に、ノードの種類typeと、ノードの名称name、ノードの値value、ノードの記述Descriptionに応じた文字列を生成して表示する。また、表示部17は、グラフ情報300に含まれる各リンクの情報に応じて、各ノードをつなぐリンクの図形矢印の図形221~226をも生成して表示する。このようにして、ユーザは、検査対象情報200に対応したグラフ情報300を知ることができる。なお、この具体例では、モデル情報がグラフ情報においてはすべて不可視情報となっているため、グラフには表示されないことになる。なお、図12A,図12Bで示される、XMLで記述されたグラフ情報300は、実際のD-CaseEditorで用いられるXMLの表記とは細部において異なっているが、実質的には同様のものである。また、グラフ情報において、ケースに含まれる各ノードの親子関係を示す方法は問わない。したがって、図12A,図12Bで示される以外のデータ構造によって、グラフ情報を示してもよいことは言うまでもない。また、そのXMLで記述されたグラフ情報300を図11で示されるように図的に表示する際に、descriptionのタグで特定される文字列の表示と、図11で示されるvalueの表示とを切り替えられるようにしてもよく、または、そうではなく、両方を一緒に表示するようにしてもよい。前者の場合であっても、コンテキストノードについては、descriptionのタグで特定される文字列を絶えず表示するようにしてもよい。次に、グラフ情報を検査対象情報に翻訳する処理について説明する。ここでは、グラフ記憶部15において、図12A,図12Bで示されるグラフ情報300が記憶されているものとする。なお、そのグラフ情報300は、例えば、ユーザが、D-CaseEditor等を用いて入力したものであってもよいステップS107~S109。そして、ユーザが、グラフ情報を検査対象情報に翻訳する旨の指示を整合性検査装置1に入力したとする。すると、その指示は受付部18で受け付けられ、翻訳部16に渡される。そして、翻訳部16は、グラフ情報を検査対象情報に翻訳するタイミングであると判断しステップS113、グラフ情報を検査対象情報に翻訳する処理を行うステップS114。具体的には、翻訳部16は、グラフ情報300のリンクの情報311~316を参照し、sourceには存在するがtargetには存在しないノード、すなわち、ルートノードを特定するステップS501。この場合には、id=001のノードがルートノードとなる。そのルートノードはディーケースのグラフのルートノードでもあるため、翻訳部16は、ケースの処理を行うステップS502。具体的には、id=001である特定したルートノードがsourceである1番目のリンクの情報315を特定し、そのsourceのノードと、targetのノードとを特定する。この場合には、sourceのノードがゴールノードであり、targetのノードがストラテジノードとなる。したがって、翻訳部16は、親ノード、子ノード=ゴールノード、ストラテジノードのパターンを特定するステップS601,S602。この場合には、リンク先がアーギュメントであるため、翻訳部16は、アーギュメントの処理を行うステップS603,S604。具体的には、アーギュメントのルートノードid=002のストラテジノードをリンク元とするリンクの情報312,314が存在するため、翻訳部16は、アーギュメントのルートノードにリンク先のノードが存在すると判断しステップS701、そのリンクのうち、1番目のリンクの情報312を特定するステップS702,S703。また、翻訳部16は、その特定したリンクのリンク先がケースであるかどうか判断するステップS704。すなわち、翻訳部16は、特定したリンクの情報312からリンク先targetのid=003を取得し、そのid=003のノードの情報303を特定する。そして、その特定したノードの情報303に含まれるノードの種類typeがゴールであるため、翻訳部16は、リンク先がケースであると判断する。そして、そのリンク先のケースの処理を行うステップS705。具体的には、翻訳部16は、処理対象であるケースのルートノードid=003のノードがsourceである1番目のリンクの情報311を特定し、そのsourceのノードと、targetのノードと関係、すなわち、親ノード、子ノード=ゴールノード、エビデンスノードのパターンを特定するステップS601,S602。この場合には、リンク先がアーギュメントであるため、翻訳部16は、アーギュメントの処理を行うステップS603,S604。具体的には、アーギュメントのルートノードid=004のエビデンスノードをリンク元とするリンクの情報が存在しないため、翻訳部16は、アーギュメントのルートノードにリンク先のノードが存在しないと判断しステップS701、そのルートノードに応じた項、すなわち、Evidence-Aを生成するステップS710。この項は、そのルートノードのノードの情報304のvalueを用いて生成される。この場合には、その項がそのままアーギュメントの項となるステップS711。その後、翻訳部16は、そのノードid=004のエビデンスノードをリンク先とするリンクの情報311のパターンゴールノード、エビデンスノードに応じた演算子∋を生成するステップS606。また、id=003のゴールノードには、それ以上のリンク先が存在しないためステップS607,S608、翻訳部16は、そのid=003のゴールノードに応じたノードの情報303を用いて、そのノードに応じた項SubGoal-Aを生成するステップS609。そして、リンク先のアーギュメントが1個であり、リンク先のアーギュメント以外の項は存在しないためステップS610、翻訳部16は、リンク先のアーギュメントの項と、ゴールノードの項とを演算子∋でつなぐケースの項を生成するステップS611。そのケースの項は、SubGoal-A∋Evidence-Aとなる。その後、翻訳部16は、そのid=003のゴールノードをリンク先とするリンクの情報312のパターンストラテジノード、ゴールノードに応じた演算子を生成し、それを一時的に図示しない記録媒体に蓄積するステップS707。また、翻訳部16は、id=002のストラテジノードをリンク元とする2番目のリンクの情報314を特定するステップS708,S709,S703。また、翻訳部16は、その特定したリンクのリンク先がid=005のゴールノードであるため、リンク先がケースであると判断するステップS704。そして、そのリンク先のケースの処理を行うステップS705。前述の処理と同様に、このケースの処理によって、翻訳部16は、id=006のエビデンスノードに対応する項と、そのエビデンスノードをリンク先とするリンクのパターンに応じた演算子∋と、そのリンクのリンク元であるid=005のゴールノードに対応する項と、そのゴールノードをリンク先とするリンクのパターンに応じた演算子とを生成し、それを一時的に図示しない記録媒体に蓄積するステップS707。その後、翻訳部16は、id=002のストラテジノードに応じた項を生成するステップS710。リンク先は、ケースの項が2個のみであるため、翻訳部16は、リンク先の2個のケースの項と、ストラテジノードの項とを演算子でそれぞれつなぐアーギュメントの項を生成するステップS711。そのアーギュメントの項は、topStragegySubGoal-A∋Evidence-ASubGoal-B∋Evidence-Bとなる。そして、id=002のストラテジノードをルートノードとするアーギュメントの処理が終了したため、翻訳部16は、そのストラテジノードがリンク先であるリンクの情報315に応じた演算子∋を生成しステップS606、さらに、全体のケースのルートノードであるid=001のゴールノードに応じた項TopGoalを生成するステップS607~S609。そして、リンク先のアーギュメントが1個であり、リンク先のアーギュメント以外の項は存在しないためステップS610、翻訳部16は、リンク先のアーギュメントの項と、ゴールノードの項とを演算子∋でつなぐケースの項を生成するステップS611。そのケースの項は、TopGoal∋topStragegySubGoal-A∋Evidence-ASubGoal-B∋Evidence-Bとなる。なお、グラフ情報300には、コンテキストノードに対応したノードの情報307と、それに応じたリンクの情報316とが存在するが、そのコンテキストの種類typeは、Context2であるため、翻訳部16は、通常の演算子CONTENT/を生成する処理を行わない。そして、そのtype=Context2のノードの情報307と、プロパティーの情報321とが存在するため、翻訳部16は、検査対象情報に追加する情報が存在すると判断しステップS503、type=Context2のノードの情報307のdescriptionmy-D-Caseが左辺となり、その左辺と、すでに生成された上述のD-Caseの記述とを等号でつなぐ。また、プロパティーの情報321からモデル情報を読み出し、検査対象情報に追加するステップS504。その結果、最終的な検査対象情報は、次のようになる。このようにして、グラフ情報から検査対象情報への翻訳が行われる。postulateTopGoalSubGoal-ASubGoal-B:SettopStrategy:SubGoal-A→SubGoal-B→TopGoalEvidence-A:SubGoal-AEvidence-B:SubGoal-Bmy-D-Case=TopGoal∋topStragegySubGoal-A∋Evidence-ASubGoal-B∋Evidence-Bこの検査対象情報は、表示部17によって表示されステップS115、ユーザは、その検査対象情報について適宜、追記や変更を行うことができる。また、検査を行うことによって、不適切な箇所を検出することもできるステップS101~S103。ここで、翻訳部16は、検査対象情報をグラフ情報に翻訳することができ、また、グラフ情報を検査対象情報に翻訳することができる。したがって、翻訳部16は、検査対象情報をグラフ情報に翻訳し、その後に、そのグラフ情報を検査対象情報に翻訳することもできる。その際に、翻訳前の検査対象情報と、グラフ情報から翻訳された検査対象情報とは、同じであってもよく、あるいは、異なってもよい。例えば、後述するように、検査対象情報をグラフ情報に翻訳する際に、実行部14による実行が行われた場合には、通常、両検査対象情報は異なるものとなる。[検査対象情報の実行]上述の具体例では、検査対象情報をグラフ情報に翻訳する際に、実行部14による実行が不要である場合について説明したが、前述のように、実行部14による実行を行った上で翻訳を行ってもよい。その場合には、例えば、検査対象記憶部11において、図13で示される検査対象情報が記憶されていたとする。この場合には、D-Caseに応じた記述は、induction-on-NGstepbase3であるが、これは、その記載の上側で定義されている生成関数プログラムinduction-on-Nと、四の引数G、step、base、3とによって記述されたものである。したがって、この図13の検査対象情報をグラフ情報に翻訳する際には、翻訳部16によってケースに応じた上記記述が特定されステップS201、実行部14によって実行が必要であると判断されてステップS202、その生成関数プログラムが実行されることになるステップS203。具体的には、引数の具体的な値がG、step、base、3であるため、生成関数プログラムinduction-on-Nを繰り返して適用することにより、次のようになる。induction-on-NGstepbase3=G3∋step2induction-on-NGstepbase2=G3∋step2G2∋step1induction-on-NGstepbase1=G3∋step2G2∋step1G1∋step0induction-on-NGstepbase0=G3∋step2G2∋step1G1∋step0G0∋baseしたがって、最終的に、図10の検査対象情報200と同様に、項と演算子とを陽に記述する形式の検査対象情報議論構造情報を得ることができ、翻訳部16は、その検査対象情報を、図14のように表示されるグラフ情報に翻訳することができる。なお、ここでは、翻訳の前にすべての項と演算子とを陽に記述する形式の議論構造情報を生成してから翻訳を行う場合について説明したが、前述のように、翻訳の処理を行いながら、逐次的に実行を行ってもよいことは言うまでもない。例えば、induction-on-NGstepbase2を翻訳する際に、それを実行してG2∋step1induction-on-NGstepbase1を得るようにし、さらに、induction-on-NGstepbase1を翻訳する際に、それを実行してG1∋step0induction-on-NGstepbase0を得るようにしてもよい。以上のように、実行部14によって、項と演算子とを陽に記述する形式の議論構造情報を生成してから、あるいは、生成しながら翻訳を行うことによって、引数の具体値を変更するだけで、最新のケースや、図的に表示したいケースに応じたグラフ情報を生成することができるメリットがある。例えば、上述の例の場合、検査対象情報におけるGstepbase3を適宜、Gstepbase2やGstepbase5などに変更し、その後に翻訳の処理を開始することによって、ユーザは、その変更後のケースに応じた有向非巡回グラフを見ることができるようになる。なお、上述のように、項と演算子とを陽に記述する形式の議論構造情報を生成する生成関数と引数の具体値とを用いて項と演算子とを陽に記述する形式の議論構造情報を生成する場合であっても、証明検査は、生成関数と引数の具体値とを用いた記述に対して実行すればよい。その証明検査においてエラーがなければ、生成関数を実行した結果に応じた適切なグラフ情報を得られることは保証されることになる。ここで、生成関数と引数の具体値とを有する検査対象情報議論構造情報を一般的に記述すれば、次のようになる。なお、前述の例との対応で言えば、induction-on-Nがgeneratorに対応し、G、step、base、3がv1,...,vnに対応する。また、generatorの型は、x1:ParameterType1→x2:ParameterType2→...xn:ParameterTypen→Gx1x2...xnすなわち、パラメータの値がv1,...,vnのときにgeneratorv1...vnを計算すると、v1,...,vnに応じたゴールGv1...vnのケースに応じた議論構造情報項や演算子を陽に記述したものであるが生成されることになる。myLatestDCase:Gv1...vnmyLatestDCase=generatorv1...vn{-DCASEmyLatestDCaseroot-}[実行の拡張1]次に、実行部14は、項や演算子を陽に記述した議論構造情報の計算を実行することに加えて、同時に通常の計算を実行することができてもよいこと、及び、そのメリットを説明する。Agdaでは、型Dと、D型の引数をとる述語GつまりG:D→Setであるから、D型の値dと、Gdの証明D-Caseに対応する議論構造pのペアの集合を値とする型ΣDGを構成することができる。ここで、関数output-and-DCase:x:ParameterType→ΣDGが定義されたとする簡単のため、引数は一とする。この関数はxの値からD型の値を計算すると同時に、その計算された値がGを満たすことの証明を返す関数となる。そこで、議論構造情報を次のようにすることによって、パラメータの値vに応じた何らかの結果myLatestOutputが計算され、それと同時に、その結果が述語Gを満たすことを示すmyLatestDCaseである議論構造情報項や演算子を陽に記述したものであるが生成されることになる。また、翻訳部16によって、その議論構造情報をグラフ情報に翻訳することもでき、その場合には、その議論構造情報を図的に表示することも可能となる。myLatest:ΣDGmyLatest=output-and-DcasevmyLatestOutput:DmyLatestOutput=first-componentmyLatestmyLatestDCase:GmyLatestOutputmyLatestDCase=second-componentmyLatest{-DCASEmyLatestDCaseroot-}この場合には、議論構造情報を実行部14が実行することにより、何らかの計算結果の値myLatestOutputと、その値が正しいことを示す議論構造myLatestDCaseとが生成されることになる。したがって、前述のように、項や演算子を陽に記述した議論構造情報を生成する場合と比較して、値が計算されていること、また、その生成された、項や演算子を陽に記述した議論構造情報が、その計算された値に関する証明となっていることが追加されていることになる。また、この場合には、値を計算するプログラムと証明議論構造情報の陽な記述を生成するプログラムとが一体になっているため、このD-Caseは本当にこの値を計算するのに使ったプログラムに基づいているのかという心配をする必要がなくなるというメリットがある。[実行の拡張2]上記をさらに拡張して、計算された値が、パラメータの具体的値との関係において正しいことを示すD-Caseを生成することもできる。この場合には、計算結果の型Dと述語Gとがパラメータの値に依存し、D:ParameterType→Setパラメータの値に応じて結果の型も変わりうることを示すG:x:ParameterType→Dx→Setパラメータの値と、結果型の値の二つを引数にとる述語、すなわち計算の入力値と出力値の間の関係、すなわちそれが成り立っていることをD-Caseで示すべきところの計算の仕様を示すとなる。そして、output-and-DCase:x:ParameterType→ΣDxGxという型付けのものが定義されたとして、次のように議論構造情報を記述することによって、結果の型Dと述語Gとがパラメータxに依存する場合に拡張することができる。myLatest:ΣDvGvmyLatest=output-and-DcasevmyLatestOutput:DvmyLatestOutput=first-componentmyLatestmyLatestDCase:GvmyLatestOutputmyLatestDCase=second-componentmyLatest{-DCASEmyLatestDCaseroot-}この場合には、議論構造情報を実行部14が実行することにより、パラメータの具体的値vに応じた型を有する何らかの値myLatestOutputと、その値が正しいことを示す、その値とvとに応じたトップゴールGvmyLatestOutputを持つ議論構造myLatestDCaseとが生成されることになる。したがって、myLatestOutputが、最新のパラメータvとの関係において正しいことを示す最新の議論構造が得られることになる。ここで、検査対象情報の実行、実行の拡張1、及び、実行の拡張2で説明した実行の対象となる議論構造情報を情報Aと呼ぶ。上記では、いかなる過程でパラメータの具体的値vを含む情報Aが検査対象記憶部11に記憶された状態に至ってもよい。情報Aの実行の契機となる、情報Aを含む検査対象情報をグラフ情報に翻訳するタイミングは、上述した通り、翻訳部16のステップS110での判断による。[実行の拡張3]パラメータの具体的値vを含む情報Aの生成と、それのグラフ情報への翻訳情報Aの実行を含むは、整合性検査装置1内において、機械的に制御されていてもよい。この制御の記述プログラムを情報Bと呼ぶ。情報Bは、情報Aのうちパラメータの具体的値以外の部分をそのまま含んでいてもよい。情報Bは、検査対象記憶部11に記憶され、実行部14によって実行されると、外部からの入力を取得し例えばその時点でのセンサー読み取り値、入力に基づいてパラメータの具体的値vを含む情報Aを検査対象記憶部11上に生成し、その情報Aに関する計算を前段までのように実行して、その計算結果である、項や演算子が陽に記述された議論構造情報をグラフ情報に翻訳する処理を行うプログラムである。また、情報Bの実行は、生成された情報Aのその他の計算結果を外部に出力してもよい例えば、前記myLatestOutputでアクチュエータを制御するなどし、入力取得から翻訳出力までの処理を繰り返してもよい。このように、情報Bが実行されることによって翻訳が行われる場合には、検査対象記憶部11において、検査対象情報をグラフ情報に変換する処理に応じた変換プログラムも記憶されており、翻訳部16は、その変換プログラムを実行することによって、検査対象情報をグラフ情報に変換すると考えてもよい。さらに、検査対象記憶部11において、実行部14による実行を行うためのプログラムも記憶されており、実行部14は、そのプログラムを実行することによって、検査対象情報を実行すると考えてもよい。あるいは、翻訳部16が実行部14の機能を用いることができることに加えて、実行部14が翻訳部16の機能を呼び出したり、実行部14が自分自身の機能を呼び出したりすることが、再帰的に可能な構成になっていると考えてもよい。なお、この実行の拡張3の場合において、情報Bにおける情報A以外の部分は、情報Aと同じ構成的型理論に基づく同じ人工言語で記述されていてもよく、あるいは、そうでなくてもよい。すなわち、検査対象情報と変換プログラムとは、構成的型理論に基づく同じ人工言語で記述されていてもよく、あるいは、そうでなくてもよい。また、検査対象情報と、実行部14が実行を行うためのプログラムとは、構成的型理論に基づく同じ人工言語で記述されていてもよく、あるいは、そうでなくてもよい。[実行の拡張4]また、前述したように、実行部14は、証明検査において、検査対象情報に含まれるプログラム、または、検査対象情報で指定される外部プログラムを実行し、その実行結果が証明検査に用いられてもよい。その場合には、例えば、炉に関するアシュランスケースに応じた検査対象情報の証明検査を行う際に、外部プログラムを実行することによって、実際の炉の温度を取得し、その取得した炉の温度を用いて、証明検査を行うこともできる。また例えば、システムに関するアシュランスケースに応じた検査対象情報の証明検査を行う際に、そのシステムの設計情報や運用実績データ等を収めたデータベースに対するクエリーを外部プログラムとして実行して、その結果に基づいて証明検査をおこなうこともできる。また例えば、あるゴールGのエビデンスEとして自動証明プログラムPによるという記述を許し、証明検査の際に外部プログラムPをGに対して実行し、その結果いかんによって元の議論構造情報G∋Eの検査結果を定めることもできる。また、そのような実行を行う場合には、検査対象情報が実行対象となるプログラムを含んでいてもよく、あるいは、外部プログラムが呼び出されるようにしてもよい。なお、Agdaにおいては、そのような外部プログラムを呼び出す機能プラグイン機構を用いた証明検査を行うことができる。そのことについては、次の文献を参照されたい。文献:YoshifumiYuasa,YoshinoriTanabe,ToshifusaSekizawa,KoichiTakahashi、VerificationoftheDeutsch-Schorr-WaiteMarkingAlgorithmwithModalLogic、SecondInternationalConference,VerifiedSoftware:Theories,Tools,ExperimentsVSTTE2008,LNCS5295,p.115-129,2008年次に、コンテキストにパラメータの情報Parametersも含まれる場合の具体例について簡単に説明する。検査対象情報が図15で示されるものであったとする。この場合には、DCaseName{Pattern}{PatternVariableDecl}は、等号の左辺であるexample-with-paramsXe1e2となる。そして、各パラメータは、X、e1、e2である。翻訳部16は、その各パラメータの型付けが、X:System、e1:Xis-designed-dependable、e2:Xis-developed-correctlyであることを、TypeSignatureである部分等号より上の3行で示されたexample-with-paramsの型から判断する。これは、Agdaのような構成的型理論の実装において一般的な技術である型推論を行うことによってなされる。したがって、ステップS206の処理において、Clauseexample-with-paramsXe1e2ParametersX:Systeme1:Xis-designed-dependablee2:Xis-developed-correctlyを含むコンテキストノードが生成されることになる。なお、前述のように、グラフ情報において、このコンテキストノードに対応するノードの情報のtypeは、Context2である。また、図15で示される検査対象情報が翻訳されたグラフ情報の表示は、図16で示されるようになる。その図16において、ルートノードの子ノードであるコンテキストノードにおいて、上述のClauseと、Parametersとが含まれている。また、上述の具体例では、グラフ情報300において、モデル情報201をプロパティーの情報321に含める場合について説明したが、そうでなくてもよい。モデル情報201に対応したコンテキストノードを生成するようにしてもよい。そのコンテキストノードも、議論構造情報におけるルートノードの子ノードとして生成されることが好適である。また、そのコンテキストノードに含まれる記述が、グラフ情報から検査対象情報への翻訳の際にモデル情報に変換されるように、そのモデル情報を含むコンテキストノードが他のコンテキストノードと区別可能になっていることが好適である。具体的には、そのコンテキストノードに対応するノードの情報において、typeをContext3とすることによって、その区別が行われるようにしてもよい。また、検査対象情報において、let構文を用いてもよい。let構文を用いることによって、議論構造情報における局所的な宣言を行うことができる。例えば、前述のD-CaseやArgumentを、次のように拡張してもよい。D-Case::=...|letFormalContext[ContextDescription]inD-CaseArgument::=...|letFormalContext[ContextDescription]inArgumentなお、...は、前述のD-CaseやArgumentの記述を示すものである。具体的には、例えば、議論構造情報202を、次のようにlet構文を用いて記述することも可能である。my-D-Case=letT1=TopGoalT2=topStrategyS1=SubGoal-AS2=SubGoal-BE1=Evidence-AE2=Evidence-BinT1∋T2S1∋E1S2∋E2上記の例では、letとinとの間において、TopGoalやtopStragegy等を、T1やT2で記述することを宣言し、in以下のD-Caseにおいて、項をT1やT2で記述している。なお、let構文を用いて局所モデル情報を記述してもよい。すなわち、letとinとの間に、局所モデル情報を含めるようにしてもよい。なお、検査対象情報をグラフ情報に翻訳する際に、このletとinとの間の記述は、in以下のD-CaseやArgumentにおけるルートノードの子ノードであるコンテキストノードに含めるようにしてもよい。その際にも、そのコンテキストノードに含まれる記述が、グラフ情報から検査対象情報への翻訳の際にlet構文に変換されるように、そのlet構文の記述を含むコンテキストノードが他のコンテキストノードと区別可能になっていることが好適である。具体的には、そのコンテキストノードに対応するノードの情報において、typeをContext4とすることによって、その区別が行われるようにしてもよい。また、検査対象情報がモジュール構造を有する例について簡単に説明する。図17A,図17Bで示される検査対象情報厳密には、検査対象情報の議論構造情報であるにおけるlet構文のletとinとの間に、openC-DefSysやopenC-SystemSafeが含まれている。そのことは、in以下において、モジュールC-DefSysやC-SystemSafeの中で記述された情報が、inに続く項の中で参照されることの宣言を意味している。なお、この例でのモジュールは、モデル情報についてのものであるが、モジュール内で記述される情報はそれに限定されないことは言うまでもない。すなわち、モジュールは、モデル情報について使用されてもよく、議論構造情報について使用されてもよい。このように、検査対象情報においてモジュールが使用される範囲は問わない。検査対象情報の記述にモジュール構造を利用することによって、ソフトウェア記述におけるモジュール構造の利点を、検査対象情報の記述に導入することができるようになる。例えば、関連する情報を一箇所にまとめることにより保守性が向上する点、パラメータ付きモジュールを定義することにより汎用性が向上する点、モジュール間のインターフェースを定めた上で各モジュールを構築することにより作業を確実に分割し、また作業結果を機械的に合成することできる点、などが挙げられる。また、アーギュメントは、上述の説明以外のパターンをも有してもよい。例えば、アーギュメントは、次のように、∀Introや、→Introなどの演算子を用いて構成されてもよい。Argument::=...|∀Intro{Domain}Lambda-D-Case|→Intro{Domain}Lambda-D-CaseLambda-D-Case::=λAgdaの変数名→D-CaseDomain::=Set型のAgda項なお、...は、前述のArgumentの記述を示すものである。また、exが変数xを含むAgda項であるとき、λ表記λx→exは、具体的値vを受け取るとevxにvを代入したときのexの値を返す関数を表すAgda項である。演算子∀Introは、∀x:D→Pxすなわち全てのD型の値xについて、Pxが成り立つPはD型の値を引数とする述語の形のゴールを示すアーギュメントの記述を構成するために用いる。構成的型理論において、この形の命題の一の証明を与えるということは、D型の任意の値xを受け取って、Pxの証明を返すような一の関数を与えることである。演算子∀Introは、第一引数として一の型D、第二引数として一のそのような関数のλ表記λx→Px∋Argumentxとをとり、ゴール∀x:D→Pxを示すアーギュメントのAgda表記∀Intro{D}λx→Px∋Argumentxを構成する。これのAgda項としての意味は、第二引数である関数自体と同じである。アーギュメントとしては、xを任意のD型の値を表す変数として導入し、ゴールPxをアーギュメントArgumentxで示すというアーギュメントである。同様に、演算子→Introは、G1→G2すなわちG1ならばG2G1とG2はゴールの形のゴールを示すアーギュメントの記述を構成するために用いる。構成的型理論において、この形の命題の一の証明を与えるということは、G1の任意の証明hを受け取って、G2の証明を返すような一の関数を与えることである。演算子→Introは、第一引数として一のゴールG1と、第二引数として一のそのような関数のλ表記λh→G2∋Argumenthとをとり、ゴールG1→G2を示すアーギュメントのAgda表記→Intro{G1}λh→G2∋Argumenthを構成する。これのAgda項としての意味は、第二引数である関数自体と同じである。アーギュメントとしては、仮にG1のエビデンスが与えられたとしてこれをhとし、G2をアーギュメントArgumenthで示すというアーギュメントである。アーギュメントArgumenthの中では、G1を示すエビデンスとしてhを用いることができることになる。それら∀Introや→Introの両方を用いた簡単な検査対象情報の例は、図18で示すものである。厳密には、図18は、議論構造情報のみを示している。図18の議論構造情報は、簡単に言えば、すべての自然数nについて、Pn→Pnを証明するため、任意の自然数nについて、Pn→Pnを証明するものである。そして、その任意の自然数nについてPn→Pnを証明するため、Pnの証明pを仮定し、その証明pを用いることによってPnの成立を証明するものである。図18で示される議論構造情報を翻訳する際には、図5のフローチャートのステップS401において、翻訳部16は、∀Intro{D}λx→tや→Intro{G1}λh→tを、ストラテジと残りのケースのパターンの一種として特定する。両者において、残りのケースはtの部分であり、それ以外の部分の情報はストラテジノードとそのストラテジノードの子となるコンテキストノードの情報に翻訳される。具体的には、ステップS401において∀Intro{D}λx→tのパターンが特定された場合には、翻訳部16は、ステップS402において、value属性がIntroduceanassumptionであるストラテジノードの情報と、description属性がAssumptionx:Dであるコンテキストノードの情報と、そのストラテジノードがsourceであり、そのコンテキストノードがtargetであるリンクの情報とを生成する。そして、翻訳部16は、ステップS402で生成されたノードはリーフでなく、残りtはケースであると判断し、tに対しケースに応じた記述の処理を行うステップS403~S405。また、ステップS401において→Intro{G1}λh→tのパターンが特定された場合には、翻訳部16は、ステップS402おいて、value属性がAssumetheantecedentであるストラテジノードの情報と、description属性がAssumptionh:G1であるコンテキストノードの情報と、そのストラテジノードがsourceであり、そのコンテキストノードがtargetであるリンクの情報とを生成する。そして、翻訳部16は、ステップS402で生成されたノードはリーフでなく、残りtはケースであると判断し、tに対しケースに応じた記述の処理を行うステップS403~S405。このようにして、図18の検査対象情報をグラフ情報に翻訳した結果は、図19で示されるようになる。なお、ストラテジノードにおけるvalueは、それら以外のものであってもよい。但し、∀Intro{D}のパターンと、→Intro{G1}のパターンとで別のものになることが好適である。グラフ情報から検査対象情報への翻訳を適切に行うことができるようにするためである。また、このようにして生成されるコンテキストノードも、他のコンテキストノードと区別可能になっていることが好適である。具体的には、そのコンテキストノードに対応するノードの情報において、typeをContext5とすることによって、その区別が行われるようにしてもよい。なお、∀Introや→Introに応じて生成されたストラテジノードをルートノードとするアーギュメントのグラフ情報を検査対象情報に翻訳する際のアーギュメントの処理図8は次のようになる。∀Introや→Introの処理に応じて生成されたコンテキストノード例えば、type属性がContext5であるノードのことを、通常のコンテキストノードと区別してAssumptionを示すコンテキストノードと呼ぶことにする。ステップS703において、リンクのパターンがストラテジノード、ゴールノードまたはストラテジノード、通常のコンテキストノードである場合は、先に説明した通りに処理を進める。リンクのパターンがストラテジノード、Assumptionを示すコンテキストノードである場合、コンテキストノードのdescription属性はAssumptionx:Dの形であり、ステップS706では、これからAgdaの変数名xとSet型のAgda項Dを生成し、ステップS707では演算子を生成しない。ステップS710では、アーギュメントのルートノードのvalue属性がIntroduceanassumptionである場合は、ストラテジの項として∀Intro{D}を生成し、Assumetheantecedentである場合は、→Intro{D}を生成する。ここで、Dは、Assumptionを示すコンテキストノードへのリンクのパターンに対してステップS706で生成した項である。ステップS711では、アーギュメントの項として、CONTEXT[コンテキストノード項1/CONTEXT[コンテキストノード項2/...CONTEXT[コンテキストノード項m/ステップS710で生成されたストラテジの項λx→ケース項]...]]を生成する。ここで、コンテキストノード項iは、通常のコンテキストノードへのリンクのパターンに対してステップS706で生成した項、ケース項は、ゴールノードへのリンクのパターンに対してステップS705で生成した項、xは、Assumptionを示すコンテキストノードへのリンクのパターンに対してステップS706で生成した変数名である。なお、そのD-Caseは、ステップS705のケースの処理によって生成したものである。このように、上記具体例で説明した以外の他の演算子や項についても、翻訳を行うことができる。また、本実施の形態で説明した以外の項や演算子についても、同様にして、適宜、検査対象情報で使用され、また、検査対象情報からグラフ情報への翻訳、または、グラフ情報から検査対象情報への翻訳が行われてもよいことは言うまでもない。なお、ここで説明したように、項とノードとが対応し、演算子とリンクとが対応するとは限らない。すなわち、翻訳時にはそれら以外の対応関係をも用いて、検査対象情報とグラフ情報との間の翻訳が行われてもよい。また、上述した具体例では、Evidence-Aを、Evidence-Bに書き間違えていた場合に、証明検査によってエラーの検出されることについて説明した。そのエラーは、推論規則の適用のしかたの誤りに関するエラーであると言うことができる。ここでは、他の例として、証明検査において、場合分けが適切でないエラーが検出されることについて説明する。まず、モデル情報の一部として、図20で示されるMachineryHazardが検査対象記憶部11で記憶されているとする。図20において、dataHazardType:Setwhere以下において、MechanicalからCombinationまでの10個のハザード種別が規定されている。また、その下に、全てのハザード種別tについてPtPはハザード種別を引数にとる述語という形のゴールを示すための一般的ストラテジArgue-over-HazardTypeが定義されている。このストラテジは、tがMechanicalハザードである場合、tがElectricalハザードである場合、...等の10の場合のサブゴールをそれぞれ示すことによってゴールを示すものである。図21A,図21Bは、検査対象記憶部11で記憶されている検査対象情報の一部を示す情報である。図21Aの5行目において、openimportMachineryHazardと記述されており、この検査対象情報において、図20のMachineryHazardが読み込まれている。また、前述の一般的ストラテジArgue-over-HazardTypeのパラメータPtに当たる具体的述語としてthazards-are-examinedが定義され、そのtを具体的なハザード種別Mechanical、Electrical、...、Combinationとした場合の10のサブゴールに対する10のサブケースの記述level2-Mechanical、level2-Electrical、...、level2-Combinationが与えられている。また、図21Bにおいて、ストラテジArgue-over-HazardTypeによる10の場合への場合分けの議論構造情報が具体的に記述されている。その議論構造に対応するグラフ情報は、図22で示されるものであり、ストラテジノードArgu-over-HazardTypeの子ノードとして、10個のハザード種別に対応した10個のゴールノードが存在している。この図21A,図21Bで示される検査対象情報について、検査部12が証明検査を行い、エラーが存在しないことがある時点で確認されたとする。その後、状況の変化に応じて、図20のMachineryHazardの定義において、図23の矢印の位置で示されるように、HazardTypeにTerrorismをさらに追加し、ストラテジArgue-over-HazardTypeの定義も、11の場合への場合分けに拡張したが、図21A,図21Bの議論構造情報を更新し忘れて、検査対象情報に不整合を導入してしまったとする。その後に、もう一度、検査部12が証明検査を行うと、この場合には、モデル情報におけるHazardTypeにはTerrorismが含まれるが、議論構造情報にはTerrorismが含まれていないため、エラーが検出されることになる。その結果、例えば、ユーザが、議論構造情報において、Terrorismに対応する記述を追加することによって、検査対象情報議論構造情報を修正し、エラーとならないようにすることができる。このように、証明検査によって、整合性の検査対象であるケースにおける場合分けがあらかじめ規定されている通りに行われているかどうかをチェックすることも可能である。次に、上述の説明以外のエラーの例として、証明検査において、数値の単位が異なっているエラーが検出されることについて説明する。まず、モデル情報の一部として、図24で示される検査対象情報が検査対象記憶部11で記憶されているとする。この検査対象では、メートル法の重量単位kgキログラムと、ヤードポンド法の重量単位lbポンドとについて、それぞれ異なる型が定義されている。したがって、ケースmyWeightisLighterThan100lb∋myEvidenceにおいては、ゴールに含まれる100lbについて、型が合わないことになる。そのため、この図24で示される検査対象情報について証明検査を行うと、図25で示されるように、エラーが検出されることになる。図25は、検査結果出力部13が表示した、証明検査の結果を示すものである。図25の上部では、エラーの箇所に下線が引かれ、その先頭にカーソルが位置することによって、エラーの箇所が明示されている。また、図25の下から5行目から下から3行目までで示される検査結果のうち、1行目図25の下から5行目を見ることによって、エラーの箇所ファイル名:行番号,コラム番号を知ることができ、3行目図25の下から3行目を見ることによって、100lbが、期待されるところの型MetricWeightを持っていることを確認する際にエラーが判明したことを知ることができ、2行目図25の下から4行目を見ることによって、その100lbの型であるImperialWeightは、MetricWeightには変換できない旨のエラーの内容を知ることができる。このように、検査対象情報において、証明検査の対象としたいものについて適宜、型を定義して記述することによって、所望のものを証明検査の対象とすることができる。また、Agda言語での正確な記述をする場合には、演算子と引数との間はすべて空白で区切られている必要があり、コロンや等号の前後に空白が必要であるが、上記具体例においては、説明の便宜上、その空白を省略した箇所がある。以上のように、本実施の形態による整合性検査装置1によれば、アシュランスケースのような整合性の検査対象であるケースの整合性を、証明検査プルーフチェックによって自動的に検査することができる。したがって、推論規則の適用のしかたが不適切であったり、あらかじめ規定されている場合分けと異なる場合分けが行われていたり、使用する単位が異なっていたりした場合には、そのエラーを検出することができる。その結果、そのエラーを修正し、整合性を有するケースを構築することができる。また、その自動的な検査を、定理証明支援系を用いて行うことによって、検査を行う独自のソフトウェアを開発する必要がなくなる。また、翻訳部16によって、人工言語で記述された検査対象情報をグラフ情報に変換することによって、その人工言語による記述に不慣れな者であっても、ケースの構造を容易に把握することができるようになる。また、グラフ情報を検査対象情報に翻訳することも可能であるため、その人工言語に精通していないユーザは、グラフ情報においてケースの編集を行い、その編集後のケースに応じたグラフ情報を検査対象情報に翻訳することによって、人工言語で記述された検査対象情報を生成することも可能である。また、そのようにして翻訳された検査対象情報に対して証明検査を行うことによって、グラフ情報において生成されたケースにエラーが存在するかどうかを確認することもできる。また、アシュランスケース等の整合性の検査対象であるケースは、最終的にはリーフであるエビデンスによって証明されることになる。したがって、エビデンスが変更された場合などには、その変更後のエビデンスを用いて検査対象情報について証明検査を行うことで、整合性の検査対象であるケースの整合性が担保されているかどうかを簡単に確認することができる。また、そのような場合には、エビデンスを入力データとして、整合性を検査していると考えることもできる。なお、本実施の形態では、特に図3~図8のフローチャートで示される翻訳に関する処理では、ケースが木構造を有する場合について説明したが、前述のように、ケースは、有向非巡回グラフの構造を有してもよい。したがって、ここでは、有向非巡回グラフの構造を有するケースに応じた検査対象情報について説明し、そのような検査対象情報をグラフ情報に翻訳する場合の処理と、また、そのようなグラフ情報を検査対象情報に翻訳する場合の処理とについて説明する。有向非巡回グラフの構造を有する場合には、あるノードが2以上の親ノードを有することになる。その場合には、図26で示されるように、検査対象情報において、let構文を用いて共有される部分グラフのルートノード、すなわち、2以上の親ノードを有するノードを共有することを宣言する。なお、そのノードを共有すると言うことは、言い換えれば、そのノードをルートノードとする部分グラフを共有することになる。具体的な記述としては、図26で示されるように、Evidence-Aが共有される場合には、そのEvidence-AをmyShareEvidenceと定義する。その定義の次の行に存在するPragma{-DCASEmySharedEvidenceshared-}は、部分グラフを共有する旨の宣言であることを示すものである。このPragmaが存在することによって、局所モデル情報等を含むlet構文と区別することができる。なお、inより後の議論構造において、2回、myShareEvidenceが出てくるが、それらは、letとinとの間で定義した通り、Evidence-Aである。なお、Agda言語を、検査対象情報を記述する人工言語として用いる具体例においては、ゴールノードやストラテジノード、エビデンスノードが2以上の親ノードを有することは想定しているが、コンテキストノードが2以上の親ノードを有することは想定していない。コンテキストノードが2以上の親ノードを有する場合には、その親ノードのすべてに共通する祖先ノードを、そのコンテキストノードの親ノードとすることによって、コンテキストノードが2以上の親ノードを有さないようにすることができるからである。また、ゴールノードの子ノードとしては、コンテキストノード以外のノードが複数存在することはないものとする。このような有向非巡回グラフの構造を有するケースに応じた検査対象情報をグラフ情報に翻訳する場合には、検査対象情報にlet構文が存在する場合に、そのlet構文がノードの共有のためのものか、それ以外のものかを判断する。その判断は、前述のPragmaを用いて判断することができる。そして、ノードの共有のためのlet構文である場合には、翻訳部16は、letとinとの間で記述されている定義図26の例では、myShareEvidence=Evidence-Aを一時的に記憶しておく。そして、myShareEvidenceの項に対応するノードを生成する処理ステップS302,S402において、翻訳部16は、すでにそのノードが存在するかどうか判断し、まだ存在しない場合には、その定義に応じてノードの生成を行う。一方、すでに存在する場合には、そのノードの生成を行わず、上位のフローチャートに戻るようにしてもよい。そのようにすることで、共有されているノードに応じた項が1回目に出てきたときには、通常通り、その項に対応するノードが生成されるが、その項の2回目以降の出現に対しては、ノード自体は生成されず、1回目の出現の際に生成されたノードへのリンクのみが生成されることになる。図26で示される検査対象情報が翻訳されたグラフ情報は、図27で示されるようになる。図27において、Evidence-Aのノードが共有されていることが分かる。次に、図27に応じたグラフ情報を検査対象情報に翻訳する場合の処理について説明する。この場合には、翻訳部16は、グラフ情報を参照し、共有されているノード、すなわち、親ノードを2以上有するノード例えば、Evidence-Aのノードが存在するかどうか判断する。具体的には、翻訳部16は、あるノードをtargetノードとする2以上のリンクの情報が存在する場合に、共有されているノードが存在すると判断してもよい。その場合には、2以上のリンクの情報によってtargetノードとされているノードが、共有されているノードとなる。そして、翻訳部16は、その共有されているノード以下の部分グラフに応じた項について、新たな名前例えば、sharedEvidenceなどを付ける定義例えば、sharedEvidence=Evidence-Aなどを生成する。その名前は、例えば、sharedと、ノードの種類を示す情報例えば、GoalやStrategy、Evidenceなどとをつなげたものであってもよい。また、その名称が重複する場合例えば、共有されるエビデンスノードが2以上存在する場合などには、その名前の最後に、適宜、1や2等の情報を付加してもよい。次に、翻訳部16は、その定義を挿入する位置ノードを特定する。その特定対象となるノードは、条件1ルートノードからの経路が一通りである条件2そのノードの子ノードに、共有されているノードの祖先であるものが2以上存在するという2個の条件を満たすノードである。その特定対象のノードを特定する方法として、例えば、次のような処理を行ってもよい。まず、判断対象のノードをルートノードとする。また、判断対象のノードの子ノードに、共有されているノードの祖先であるノードが1個存在するのか、あるいは、2個以上存在するのか判断する。そして、2個以上存在する場合には、判断対象のノードが特定対象のノードとなる。一方、1個存在する場合には、その1個のノードこのノードは、ルートノードの子ノードであるを判断対象のノードとする。また、前述の処理と同様に、その判断対象のノードの子ノードに、共有されているノードの祖先であるノードが1個存在するのか、あるいは、2個以上存在するのか判断する。そして、2個以上存在する場合には、判断対象のノードが特定対象のノードとなる。一方、1個存在する場合には、その1個のノードを判断対象のノードとする。この処理を、判断対象のノードが特定対象のノードとなるまで繰り返して実行すればよいことになる。そして、特定対象のノードが特定できた後には、前述の説明と同様に、グラフ情報から検査対象情報を生成する処理を行う。その際に、共有されているノードについては、定義した名称の項を生成するものとする。また、図6で示される検査対象への翻訳の処理が終了した後に、特定対象ノード以下の部分グラフに応じた項tを、あらかじめ生成していた共有部分グラフに応じた項の定義sharedEvidence=共有部分グラフの項を含むlet構文の項で置き換える。具体的には、項tを、項letsharedEvidence=共有部分グラフの項{-DCASEsharedEvidenceshared-}intで置き換える。このようにして、有向非巡回グラフの構造を有するグラフ情報から検査対象情報への翻訳を行うことができる。なお、検査対象情報におけるlet構文の生成は、検査対象情報において順次、項や演算子を追加する際に行ってもよい。すなわち、特定対象のノードに応じた項が生成された時点で、共有部分グラフに応じた項の定義を含むlet構文を生成し、さらに、それ以降の項や演算子の生成の処理を継続するようにしてもよい。ここで、図26,図27の例の場合には、特定対象のノードは、topStragegyに応じたストラテジノードである。また、本実施の形態において、メタ変数を用いることによって、整合性の検査対象であるケースに応じた未完成の検査対象情報や未完成のグラフ情報についても証明検査を行うようにしてもよい。そのためには、検査対象情報を記述する人工言語として、対話型証明支援系の人工言語を用いることが好適である。これは、対話型証明支援系の人工言語であれば、検査部12が、メタ変数を含む項を有する検査対象情報についても証明検査プルーフチェックを行うことができるからである。なお、前述のAgda言語は、対話型証明支援系の人工言語の一例である。ここで、メタ変数とは、未完成作成途中の項の中で、最終的には正式な記述がなされる部分を示すプレースホールダ、すなわち、この部分は、今は未定の穴開き状態であるが、将来は具体的な部分項で埋められる部分であるという部分を示すプレースホールダである。なお、そのメタ変数を含む検査対象情報は、グラフ情報から翻訳されたものであってもよく、あるいは、そうでなくてもよい。後者の場合としては、例えば、ユーザが検査対象情報を人工言語での記述として入力する際に、メタ変数を用いる場合があり得る。このように、メタ変数を用いて記述された検査対象情報について証明検査を行うことによって、作成途中の検査対象情報あるいは、その検査対象情報の翻訳元の作成途中のグラフ情報に誤りがあるかどうかを確認することができ、誤りがある場合には、適宜、その誤りを解消するように検査対象情報あるいは、その検査対象情報の翻訳元のグラフ情報を修正することができる。したがって、メタ変数を含む検査対象情報の証明検査は、検査対象情報に変更が加えられるごとに行われることが好適である。また、グラフ情報が作成されている場合には、作成途中のグラフ情報に変更が加えられるごとに、翻訳と、その翻訳後のメタ変数の項を含む検査対象情報の証明検査とが行われることが好適である。なお、メタ変数を含んだ検査対象情報の証明検査については、次の情報を参照されたい。情報:UlfNorell.Typecheckinginthepresenceofmeta-variables.InTYPES2007,CividaledelFriuli,Italy,2007年5月conferenceurl:http://users.dimi.uniud.it/types07/情報:CatarinaCoquandandThierryCoquand.Structuredtypetheory.InWorkshoponLogicalFrameworksandMeta-languages,Paris,France,1999年9月workshopurl:http://www.site.uottawa.ca/~afelty/LFM99/index.htmlここで、メタ変数を含む検査対象情報や、グラフ情報の例について簡単に説明する。図28は、メタ変数を含む検査対象情報の一例である。図28において、メタ変数{}が用いられている。したがって、この場合には、ゴールノードの項TopGoal以下が未定である。なお、図28の検査対象情報は、図29に応じたグラフ情報が翻訳されたものであると考えてもよい。図29では、ゴールノードの子ノード側が未定であるため、value=を有するエビデンスノードが設定されている。翻訳部16は、value=を有するエビデンスノードを、メタ変数{}の項に変換するものとする。なお、検査部12が、図28の検査対象情報について証明検査を行ったとしても、エラーは検出されない。その証明検査は、対話型証明支援系のプルーフチェッカーによる証明検査である。次に、ユーザが、ゴールノードの項TopGoalに対して、ストラテジノードの項等を新たに設定し、検査対象情報が図30で示されるようになったとする。なお、この場合にも、ユーザが、D-CaseEditor等を用いてグラフ情報を変更し、その結果、図31に応じたグラフ情報が生成され、そのグラフ情報の翻訳結果が図30で示される検査対象情報であると考えてもよい。図30の検査対象情報では、サブゴールノードの項SubGoal-A、SubGoal-B以下が未定であり、その箇所にメタ変数{}がそれぞれ設定されている。この場合にも、図30の検査対象情報について証明検査が行われても、エラーは検出されない。さらに、ユーザが、サブゴールノードの項SubGoal-Aに対して、エビデンスノードの項Evidence-Aを新たに設定し、検査対象情報が図32のようになったとする。なお、この場合にも、ユーザが、D-CaseEditor等を用いてグラフ情報を変更し、その結果、図33に応じたグラフ情報が生成され、そのグラフ情報の翻訳結果が図32で示される検査対象情報であると考えてもよい。この場合にも、図32の検査対象情報について証明検査が行われても、エラーは検出されない。一方、ユーザが、図30で示される検査対象情報において、図34で示されるように、サブゴールノードの項SubGoal-Aに対応したエビデンスノードの項として、Evidence-Bを入力しようとしたとする。この場合には、SubGoal-Aと、Evidence-Bとの型が異なるため、検査部12は、証明検査の結果としてエラーを返し、入力の受け付けを拒否する。そして、ユーザは、検査結果出力部13が表示した図35の下部3行で示される検査結果を見ることによって、エラーの箇所一行目に記述されているファイル名:行番号,コラム番号と、そのエラーの内容三行目に記述されている入力された項Evidence-Bが期待されるところの型SubGoal-Aを持っていることを確認する際にエラーが判明した、二行目に記述されている入力された項の型SubGoal-Bは、SubGoal-Aには変換できない両者をSet型の要素と見たときとを知ることができるようになる。その結果、ユーザは、そのエラーを解消するために、検査対象情報を図32で示されるように変更することができる。なお、メタ変数に入れようとする項は、メタ変数を含んでいてもよく、あるいは、含んでいなくてもよい。図34では、メタ変数を含むエビデンスノードの項Evidence-Bが設定されている場合について示している。ユーザが、人工言語での記述において、メタ変数に型の合わない項を入力しようとする場合は上のように入力操作自体が拒否されるが、D-CaseEditor等での誤った図的編集は、それ自体は拒否されず、翻訳を経て証明検査をした時点で誤りが判明する。この場合でも、未完成のケースの整合性を検査できることにより、早い段階で誤りを見つけることができる。ユーザが、図31に応じたグラフ情報において、図36で示されるように、サブゴールノードSubGoal-Aに対応したエビデンスノードとして、Evidence-Bを設定したとする。ユーザは、ケースが未完成なまま、そのグラフ情報を、翻訳部16によって、図37で示される検査対象情報に翻訳できる。この場合にも、SubGoal-Aと、Evidence-Bとの型が異なるため、検査部12は、証明検査の結果としてエラーを返す。そして、ユーザは、検査結果出力部13が表示した図38で示される検査結果を見ることによって、エラーの箇所と、そのエラーの内容とを知ることができるようになる。その結果、ユーザは、そのエラーを解消するために、検査対象情報を図32で示されるように変更することができる。上記説明のように、検査対象情報において、メタ変数を含む項の記載を許容し、そのメタ変数を含む検査対象情報についても証明検査を行うことによって、作成途中の検査対象情報や、作成途中のグラフ情報に誤りがあるかどうかを確認することができる。そして、誤りがあれば、それを訂正することによって、適切な検査対象情報やグラフ情報にすることができる。一方、誤りがなければ、その後に適切に検査対象情報やグラフ情報を構築することによって、誤りのない検査対象情報やグラフ情報を構築できる可能性のあることを知ることができる。なお、上記説明において、グラフ情報から検査対象情報への翻訳時のモデル情報の取り扱いについて特に言及しなかったが、そのモデル情報は、前述のように、例えば、グラフ情報において不可視情報として存在し、その不可視情報であるモデル情報が検査対象情報に含まれるようになってもよく、グラフ情報において、コンテキストノードの内容によってモデル情報が設定され、そのモデル情報が検査対象情報に含まれるようになってもよく、または、グラフ情報から検査対象情報への翻訳時にはモデル情報が生成されず、その翻訳の後に、モデル情報を別途に人工言語での記述として入力するようにしてもよい。また、上記説明においては、メタ変数を含むグラフ情報としては、メタ変数のみからなるエビデンスノードを持つグラフ情報について説明したが、そうでなくてもよい。例えば、ゴールノードあるいはストラテジノードの項がメタ変数であってもよく、またはそれらの項自体はメタ変数でなくそれらの項の一部としてメタ変数が現れてもよい。またあるいは、グラフ情報の構成要素としてノードとリンクだけでなく部分グラフも認めるグラフ情報の表記において、メタ変数を未確定部分グラフに対応付けることによって、未確定アーギュメントや未確定ケースを扱ってもよい。また、上記説明で参照した一連の各検査対象情報において、検査対象情報ごとにモジュール名が異なっていたり、検査対象情報ごとに異なるコメントが記載されていたりするが、それらは時系列中の時点々々での様態を記録するための便宜上のものであり、同じモジュール名が使用され、コメントが存在しないと考えてもよい。また、本実施の形態による整合性検査装置1では、実行部14を備え、検査対象情報を実行する場合について説明したが、そうでなくてもよい。検査対象情報に関する実行を行わなくてもよい場合には、整合性検査装置1は、実行部14を備えていなくてもよい。また、検査対象情報に関する実行を行わない場合には、検査対象情報は、構成的型理論ではない型理論に基づく人工言語で記述されたものであってもよい。また、本実施の形態では、検査対象情報からグラフ情報への翻訳と、グラフ情報から検査対象情報への翻訳との両方を行う場合について説明したが、そうでなくてもよい。翻訳部16は、いずれか一方の翻訳を行うものであってもよい。また、翻訳を行わなくてもよい場合には、整合性検査装置1は、翻訳部16やグラフ記憶部15を備えていなくてもよい。また、本実施の形態では、整合性検査装置1が表示部17や受付部18を備える構成について説明したが、そうでなくてもよい。整合性検査装置1が表示部17を有さない場合には、整合性検査装置1は、例えば、検査対象記憶部11で記憶されている検査対象情報にエラーが存在するかどうかを検査するためだけの装置であってもよい。また、整合性検査装置1が受付部18を有さない場合には、整合性検査装置1は、例えば、外部から着脱可能な記録媒体等によって提供された検査対象情報にエラーが存在するかどうかを検査する装置であってもよい。また、本実施の形態で説明したノードの種類、演算子や項の種類は一例であり、それら以外のノードの種類や、演算子や項の種類が存在してもよいことは言うまでもない。また、アシュランスケース等の整合性の検査対象であるケースが有する情報のうち、Agda等の人工言語で記述する範囲、すなわち、検査対象情報で記述する範囲を多くすればするほど、整合性の検査対象もより広がることになる。したがって、より多くの範囲を検査対象情報において記述することが好適である。また、本実施の形態では、モデル情報がpostulateの宣言のみを有する場合について主に説明したが、モデル情報には、それ以外の宣言が含まれてもよいことは言うまでもない。モデル情報は、例えば、postulate以外の種類の宣言である、データ型定義、レコード型定義、関数定義、または、他のモジュールのインポート宣言等を含んでいてもよい。また、上記実施の形態では、整合性検査装置1がスタンドアロンである場合について説明したが、整合性検査装置1は、スタンドアロンの装置であってもよく、サーバクライアントシステムにおけるサーバ装置であってもよい。後者の場合には、出力部や表示部、受付部は、通信回線を介して情報を出力したり、情報を表示したり、入力を受け付けたりしてもよい。また、上記実施の形態において、各処理または各機能は、単一の装置または単一のシステムによって集中処理されることによって実現されてもよく、あるいは、複数の装置または複数のシステムによって分散処理されることによって実現されてもよい。また、上記実施の形態において、各構成要素間で行われる情報の受け渡しは、例えば、その情報の受け渡しを行う2個の構成要素が物理的に異なるものである場合には、一方の構成要素による情報の出力と、他方の構成要素による情報の受け付けとによって行われてもよく、あるいは、その情報の受け渡しを行う2個の構成要素が物理的に同じものである場合には、一方の構成要素に対応する処理のフェーズから、他方の構成要素に対応する処理のフェーズに移ることによって行われてもよい。また、上記実施の形態において、各構成要素が実行する処理に関係する情報、例えば、各構成要素が受け付けたり、取得したり、選択したり、生成したり、送信したり、受信したりした情報や、各構成要素が処理で用いるしきい値や数式、アドレス等の情報等は、上記説明で明記していない場合であっても、図示しない記録媒体において、一時的に、あるいは長期にわたって保持されていてもよい。また、その図示しない記録媒体への情報の蓄積を、各構成要素、あるいは、図示しない蓄積部が行ってもよい。また、その図示しない記録媒体からの情報の読み出しを、各構成要素、あるいは、図示しない読み出し部が行ってもよい。また、上記実施の形態において、各構成要素等で用いられる情報、例えば、各構成要素が処理で用いるしきい値やアドレス、各種の設定値等の情報がユーザによって変更されてもよい場合には、上記説明で明記していない場合であっても、ユーザが適宜、それらの情報を変更できるようにしてもよく、あるいは、そうでなくてもよい。それらの情報をユーザが変更可能な場合には、その変更は、例えば、ユーザからの変更指示を受け付ける図示しない受付部と、その変更指示に応じて情報を変更する図示しない変更部とによって実現されてもよい。その図示しない受付部による変更指示の受け付けは、例えば、入力デバイスからの受け付けでもよく、通信回線を介して送信された情報の受信でもよく、所定の記録媒体から読み出された情報の受け付けでもよい。また、上記実施の形態において、整合性検査装置1に含まれる2以上の構成要素が通信デバイスや入力デバイス等を有する場合に、2以上の構成要素が物理的に単一のデバイスを有してもよく、あるいは、別々のデバイスを有してもよい。また、上記実施の形態において、各構成要素は専用のハードウェアにより構成されてもよく、あるいは、ソフトウェアにより実現可能な構成要素については、プログラムを実行することによって実現されてもよい。例えば、ハードディスクや半導体メモリ等の記録媒体に記録されたソフトウェアプログラムをCPU等のプログラム実行部が読み出して実行することによって、各構成要素が実現され得る。なお、上記実施の形態における整合性検査装置1を実現するソフトウェアは、以下のようなプログラムである。つまり、このプログラムは、目的に対応するゴールノードと、目的を立証するための根拠に対応するエビデンスノードと、一のゴールノードを一以上のゴールノードに分解するストラテジノードとを含む有向非巡回グラフの構造を有する、整合性の検査対象であるケースが、各ノードに応じた項と、各ノードの親子関係に応じた演算子とを用いて記述された情報であり、証明検査の対象となる人工言語により記述された情報である検査対象情報が記憶される検査対象記憶部にアクセス可能なコンピュータを、検査対象情報に対して証明検査を行う検査部、検査部による証明検査の結果を出力する検査結果出力部として機能させるためのプログラムである。なお、上記プログラムにおいて、上記プログラムが実現する機能には、ハードウェアでしか実現できない機能は含まれない。例えば、情報を出力する出力部などにおけるモデムやインターフェースカードなどのハードウェアでしか実現できない機能は、上記プログラムが実現する機能には少なくとも含まれない。また、このプログラムは、サーバなどからダウンロードされることによって実行されてもよく、所定の記録媒体例えば、CD-ROMなどの光ディスクや磁気ディスク、半導体メモリなどに記録されたプログラムが読み出されることによって実行されてもよい。また、このプログラムは、プログラムプロダクトを構成するプログラムとして用いられてもよい。また、このプログラムを実行するコンピュータは、単数であってもよく、複数であってもよい。すなわち、集中処理を行ってもよく、あるいは分散処理を行ってもよい。図39は、上記プログラムを実行して、上記実施の形態による整合性検査装置1を実現するコンピュータの外観の一例を示す模式図である。上記実施の形態は、コンピュータハードウェア及びその上で実行されるコンピュータプログラムによって実現されうる。図39において、コンピュータシステム900は、CD-ROMCompactDiskReadOnlyMemoryドライブ905、FDFloppy登録商標Diskドライブ906を含むコンピュータ901と、キーボード902と、マウス903と、モニタ904とを備える。図40は、コンピュータシステム900の内部構成を示す図である。図40において、コンピュータ901は、CD-ROMドライブ905、FDドライブ906に加えて、MPUMicroProcessingUnit911と、ブートアッププログラム等のプログラムを記憶するためのROM912と、MPU911に接続され、アプリケーションプログラムの命令を一時的に記憶すると共に、一時記憶空間を提供するRAMRandomAccessMemory913と、アプリケーションプログラム、システムプログラム、及びデータを記憶するハードディスク914と、MPU911、ROM912等を相互に接続するバス915とを備える。なお、コンピュータ901は、LANやWAN等への接続を提供する図示しないネットワークカードを含んでいてもよい。コンピュータシステム900に、上記実施の形態による整合性検査装置1の機能を実行させるプログラムは、CD-ROM921、またはFD922に記憶されて、CD-ROMドライブ905、またはFDドライブ906に挿入され、ハードディスク914に転送されてもよい。これに代えて、そのプログラムは、図示しないネットワークを介してコンピュータ901に送信され、ハードディスク914に記憶されてもよい。プログラムは実行の際にRAM913にロードされる。なお、プログラムは、CD-ROM921やFD922、またはネットワークから直接、ロードされてもよい。プログラムは、コンピュータ901に、上記実施の形態による整合性検査装置1の機能を実行させるオペレーティングシステムOS、またはサードパーティプログラム等を必ずしも含んでいなくてもよい。プログラムは、制御された態様で適切な機能モジュールを呼び出し、所望の結果が得られるようにする命令の部分のみを含んでいてもよい。コンピュータシステム900がどのように動作するのかについては周知であり、詳細な説明は省略する。また、本発明は、以上の実施の形態に限定されることなく、種々の変更が可能であり、それらも本発明の範囲内に包含されるものであることは言うまでもない。"