時間の論理の語モデルに対する同値性判定手続きの実現

情報処理学会

書誌事項

タイトル別名
  • Implementation of a Decision Procedure of the Equivalence in Word Models for logic for Time

この論文をさがす

説明

近年、プログラム検証への期待から時相論理やその拡張をはじめとして、時間の概念を取り入れた論理の研究が盛んに行われている。このような体系での離散時間における真理値の遷移を正則表現で表すことにより、論理式の同値性を正則表現の同値性で判定することができる。この正則表現の同値性判定には決定手続きがあり、自動化が可能である。また、決定手続きの計算は手間がかかることが多く、自動化の意義も大きい。ここでは決定手続き、論理命題から正則表現への変換規則を示す。

収録刊行物

詳細情報 詳細情報について

問題の指摘

ページトップへ