Art

J-GLOBAL ID：202002218400601685   Reference number：20A0053995

Extending Rewriting Induction to Existentially Quantified Equations

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

Author (3)： NISHIE KAZUSHI (名古屋大 大学院情報学研究科) ,  NISHIDA NAOKI (名古屋大 大学院情報学研究科) ,  SAKAI MASAHIKO (名古屋大 大学院情報学研究科)
Material： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
Volume： 119  Issue： 246(SS2019 13-24)(Web)  Page： 25-30 (WEB ONLY)  Publication year： Oct. 17, 2019 
JST Material Number： S0532B  ISSN： 0913-5685  Document type： Proceedings
Article type： 原著論文  Country of issue： Japan (JPN)  Language： JAPANESE (JA)

Thesaurus term： *term rewriting system ,  quantifier ,  proof (evidence) ,  method ,  theorem proving ,  *program verification ,  inequality ,  computation model ,  recursive method
Semi thesaurus term： quantifier

JST classification (1)： Theory of computation  (JB02000A)

Reference (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.

Terms in the title (5)： 限量子 ,  証明 ,  書換え ,  帰納法 ,  拡張