Implementing the Zc Logic in Ergo

Mark Utting; Steve Reeves

Back

Conference paper

Peer reviewed

Implementing the Zc Logic in Ergo

Mark Utting and Steve Reeves

International workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, 3rd (Norwich, United Kingdom, 13-Jul-2000)

2000

Files and links (1)

url

http://web.archive.org/web/20010503231055/http://www.sys.uea.ac.uk/RTA2000/papers.htmlView

Webpage

Abstract

Computer Software

In this paper we introduce and investigate a logic for the schema calculus of Z. The schema calculus is arguably the reason for Z's popularity but so far no true calculus (a sound system of rules for reasoning about schema expressions) has been given. Presentations thus far have either failed to provide a calculus (e.g. the draft standard [3]) or have fallen back on informal descriptions at a syntactic level (most text books e.g. [7]). Once the calculus is established we introduce a derived equational logic which enables us to formalise properly the informal notations of schema expression equality to be found in the literature.

Details

Title: Implementing the Zc Logic in Ergo
Authors: Mark Utting (Author) - University of Waikato, New Zealand
Steve Reeves (Author) - University of Waikato, New Zealand
Conference details: International workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, 3rd (Norwich, United Kingdom, 13-Jul-2000)
Date published: 2000
Organisation Unit: School of Science and Engineering - Legacy; University of the Sunshine Coast, Queensland
Language: English
Record Identifier: 99449162902621
Output Type: Conference paper

Metrics

458 Record Views