文献

J-GLOBAL ID：202102279542015466   整理番号：21A2975907

定理証明支援系Coqによるグラフ書換え言語の性質証明

Proving Properties of Graph Rewriting Languages with the Coq Proof Assistant.

著者 (2件)： 山本直輝 (早稲田大) ,  上田和紀 (早稲田大)
資料名： 日本ソフトウェア科学会大会講演論文集(Web)  (Proceeding of the JSSST Annual Conference (Web))
巻： 38th  ページ： ROMBUNNO.2-L (WEB ONLY)  発行年： 2021年 
JST資料番号： U1746A  ISSN： 1349-3515  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： ・グラフ書換言語LMNtalは,プログラミング言語とモデリング言語の側面を兼備。
・LMNtal言語の項上の同値関係(構造合同関係)とグラフ理論におけるグラフ同型性の対応は不明確。
・ここでは,その不明確性を解消するために,定理証明系Coq上で抽象構文と意味論を実装し,LMNtal言語の性質を証明。

シソーラス用語： 定理証明 ,  *項書換え系 ,  *プログラミング言語 ,  応用向き言語 ,  同値関係 ,  グラフ理論 ,  抽象 ,  意味論 ,  Coq【言語】
準シソーラス用語： グラフ書換え ,  プログラム意味論 ,  モデリング言語

分類 (2件)： 数理言語学  (JB05000V) ,  応用プログラミング言語  (JD03052Y)

タイトルに関連する用語 (6件)： 定理証明 ,  支援 ,  グラフ書換え ,  言語 ,  性質 ,  証明