著者

佐藤 洸一 菊池 健太郎 青戸 等人 外山 芳人

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.32, no.1, pp.1_179-1_193, 2015

---

項書き換えシステム上の帰納的定理の自動証明手法として書き換え帰納法(Reddy, 1989)が提案されている.しかし,書き換え帰納法は末尾再帰による関数定義が含まれると有効に働かない場合が多い.一方,プログラムの自動検証を容易にすることを目的としたプログラム変換法として,文脈移動法および文脈分割法(Giesl, 2000)が提案されている.これらの手法は,末尾再帰プログラムを自動検証に適した単純再帰プログラムへと変換する.本論文では,項書き換えシステムに対する文脈移動法・文脈分割法の正当性を証明し,それらが書き換え帰納法による帰納的定理の証明に有効であることを明らかにする.

著者

中嶋 辰成 青戸 等人 外山 芳人

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.31, no.3, pp.3_294-3_306, 2014-07-25 (Released:2014-09-10)

---

等式論理において,自然数やリストなどのデータ構造上で成立する等式を帰納的定理とよぶ.与えられた等式が等式論理の帰納的定理であるか否かは一般に決定不能であるが,いくつかの部分クラスに対する決定手続きが知られている.FalkeとKapur (2006)が与えた決定手続きは書き換え帰納法に基づく.一方,外山(2002)は,帰納的定理判定問題を2つの抽象リダクションシステムの等価性判定問題としてとらえることで,書き換え帰納法が帰納的定理の決定手続きとなるための十分条件を示した.しかし,この両者が保証している決定可能な帰納的定理のクラス間には包含関係がない.そこで,本論文ではこれら2つのアプローチを組み合わせることにより,従来保証されていた決定可能な帰納的定理のクラスを拡張する.

著者

小野 寛晰 青戸 等人 鹿島 亮 石原 哉 外山 芳人 WOLTER Frank 酒井 正彦

出版者

北陸先端科学技術大学院大学

雑誌

基盤研究(C)

巻号頁・発行日

1996

---

本研究の目標は、計算機科学に現われる数理論理学の問題を理論と応用の両面から解明しようとするものである。本年度に得られた成果のうちの主要なものを以下にあげる。1.代数的手法による縮約のない部分構造論理の一般論の展開(小野)2.部分構造論理におけるMaksimovaの変数分離の原理の研究(小野)3.直感主義的様相論理の研究(青戸、小野)4.項書き換え系における停止性および合流性に関する研究と関数型プログラム言語への応用(外山、青戸)5.弱い含意命題論理に対する証明論(鹿島)6.構成的数学の展開(石原)1)の縮約規則をもたない論理の一般論については、小野はその成果をポーランド、スウェーデン、スペイン、ドイツで発表した。また北陸先端科学技術大学院大学において、オーストラリアのM.Bunder博士、R.Gore博士およびアメリカのA.Scedrov教授とそれぞれ部分構造論理に関する共同研究をおこなった。2)については、いくつかの部分構造論理に対しMaksimovaの原理を証明論的手法により証明した。このようなアプローチはこの研究が始めてである。3)の直観主義様相論理については、青戸がその有限モデル性についての興味深い結果を示した。4)の項書き換え系とその応用については、外山と青戸が精力的に研究をおこない、優れた成果をおさめている。弱い含意論理におけるcut elimination theoremについては鹿島が、また構成的数学については石原がいくつかの成果をあげた。