## First-order dynamic logic |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Other editions - View all

### Common terms and phrases

A-equivalent A-valid a)true a€CF a€RG abbreviate arithmetical completeness arithmetical universe array-DL asserts assignments and tests Assume atomic formula augmented AX(U axiom system binary relation CFDL Chapter class of programs complete axiomatization computation trees Computer Science concepts construct defined definition denote derived rule deterministic Dijkstra Diverging and Failing domain Dynamic Logic Edited elements EPDL equivalent execution fact faila failure false finite first-order formula function symbol guarded commands language hence Hoare's holds iff Il=loopa Il=P induction inference rules intuition leaf leaf labeled Lemma loop loopa method modal logic natural numbers nondeterministic Note notion obtain partial correctness pct(a,I predicate symbol premises programming language properties propositional provable prove r.e. programs random-DL reasoning recursive programs regular expressions regular programs relative completeness respectively satisfy Section Seiten semantics term t(X terminate Theorem 3.1 total correctness true U-complete U-expressive uninterpreted variables weakest precondition Winklmann wpBG