We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.
We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.
Published online by Cambridge University Press: 24 October 2009
EXPANDER is a proof support system for reasoning about data type specifications and declarative programs. EXPANDER applies the rules of inductive expansion (cf. Chapter 5) to correctness conditions that are given as single Gentzen clauses or sets of guarded Horn clauses (cf. Chapter 2). The system provides a kernel for special-purpose theorem provers, which are tailored to restricted application areas and implement specific proof plans, strategies or tactics. It is written in the functional language SML/NJ.
EXPANDER executes single inference steps. Each proof is a sequence of goal sets. The user has full control over the proof process. He may backtrack the sequence, interactively modify the underlying specification and add lemmas or induction orderings suggested by subgoals obtained so far. When a proof has been finished, the system can generate the theorems actually proved and, if necessary, the remaining subconjectures.
We first describe the kind of specifications that can be processed, then present the commands currently provided and, finally, document the implementation. The latter serves for illustrating the suitability of functional languages for encoding deductive methods.
The specifications
Specifications to be processed by EXPANDER are generated by the following context-free grammar in extended Backus-Naur form, i.e., [_], *, | denote the usual operators for building regular expressions. Key words are enclosed in “…”.
To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.
Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.
Find out more about the Kindle Personal Document Service.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.
