What people are saying - Write a review
We haven't found any reviews in the usual places.
Regular Propositional Dynamic Logic PDL
6 other sections not shown
Other editions - View all
A-equivalent A-valid a>true abbreviate aeCF aeRG arithmetical completeness arithmetical universe asserts assignment x«-e assignments and tests Assume atomic formula augmented AX(U axiom system binary relations CF"DL CFDL CFDL-wff CFDL+ Chapter class of programs complete axiomatization computation trees concepts construct defined definition denote derived rule Dijkstra diverging and failing domain dynamic logic Edited elements EPDL equivalent execution exists an L-wff expressive fact faila false finite first-order formula function symbol guarded commands language hence Hoare's holds iff induction inference rules infinite path intuition leaf leaf labeled Lemma loopa method natural numbers nondeterministic Note notion obtain partial correctness predicate symbol premises program-free programming language properties provable prove r.e. programs random-DL reasoning recursive programs regular expressions regular programs relative completeness respectively satisfy Section Seiten semantics term r(X terminate Theorem 3.1 total correctness true U-complete U-expressive uninterpreted valid DL-wffs variables weakest precondition