Mechanical Reasoning about Families of UTP Theories | Zendy

Frank Zeyda | Zendy; Ana Cavalcanti | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Mechanical Reasoning about Families of UTP Theories

Author(s) -

Frank Zeyda,

Ana Cavalcanti

Publication year - 2009

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2009.05.055

Subject(s) - embedding , encoding (memory) , automated theorem proving , computer science , programming language , theoretical computer science , alphabet , type theory , type (biology) , artificial intelligence , philosophy , ecology , linguistics , biology

In this paper we present a semantic embedding of Hoare and He's Unifying Theories of Programming (UTP) framework into the ProofPower-Z theorem prover; it concisely captures the notion of UTP theory, theory instantiation, and, additionally, type restrictions on the alphabet. We show how the encoding can be used to reason about UTP theories and their predicates, including models of particular specifications and programs. We support encoding and reasoning about combinations of elements of collections of theory instantiations, as typically found in UTP models of particular specifications and programs

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research