文献

J-GLOBAL ID：202002218400601685   整理番号：20A0053995

存在限量子付き等式を証明するための書換え帰納法の拡張

Extending Rewriting Induction to Existentially Quantified Equations

著者 (3件)： 西江一志 (名古屋大 大学院情報学研究科) ,  西田直樹 (名古屋大 大学院情報学研究科) ,  酒井正彦 (名古屋大 大学院情報学研究科)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 119  号： 246(SS2019 13-24)(Web)  ページ： 25-30 (WEB ONLY)  発行年： 2019年10月17日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本稿では,等式を証明するための書換え帰納法を存在限量子付き等式を証明できるように拡張する.具体的にはまず,論理制約付き項書換え系の書換え規則の右辺に存在限量子を持つ項を許すように拡張する.次に,存在限量子付き等式を形式化し,書換え帰納法を拡張する.最後に,不等式を存在限量子付き等式に帰着して証明する例を示す.(著者抄録)

シソーラス用語： *項書換え系 ,  量化記号 ,  証明 ,  方式 ,  定理証明 ,  *プログラム検証 ,  不等式 ,  計算モデル ,  帰納法
準シソーラス用語： 限量子

分類 (1件)： 計算理論  (JB02000A)

引用文献 (12件)：

• Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1988.
• Stephan Falke and Deepak Kapur. A term rewriting approach to the automated termination analysis of imperative programs. In Renate A. Schmidt, editor, Proceedings of the 22nd International Conference on Automated Deduction, Vol. 5663 of Lecture Notes in Computer Science, pp. 277-293. Springer, 2009.
• Stephan Falke, Deepak Kapur, and Carsten Sinz. Termination analysis of C programs using compiler intermediate languages. In Manfred Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, Vol. 10 of LIPIcs, pp. 41-50. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2011.
• Carsten Fuhs, Cynthia Kop, and Naoki Nishida. Verifying procedural programs via constrained rewriting induction. ACM Transactions on Computational Logic, Vol. 18, No. 2, pp. 14:1-14:50, 2017.
• Cynthia Kop. Termination of LCTRSs. In Proceedings of the 13th International Workshop on Termination, pp. 59-63, 2013.

タイトルに関連する用語 (5件)： 限量子 ,  証明 ,  書換え ,  帰納法 ,  拡張