Implementation of a Decision Procedure of the Equivalence in Word Models for logic for Time

IPSJ

Bibliographic Information

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

Search this article

Description

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

Journal

Details 詳細情報について

Report a problem

Back to top