EXPRESSIBILITY OF THE SEMANTICS OF SEQUENTIAL PROGRAMS IN FIRST-ORDER LOGIC
Hardi Hungar · Fundamenta Informaticae · 1994
The notion of an expressive interpretation was originally introduced by Cook in order to formulate completeness results for Hoare-style proof systems. An interpretation is called expressive for a programming language if the input/output relation of e