Genesis Z-Tool

Thread View: comp.specification

1 messages

[T] Back to Threads [V] Tree View [G] Group Articles

1 total messages Started by Tony Cant Thu, 20 Aug 1992 17:04

#89

Author: Tony Cant
Date: Thu, 20 Aug 1992 17:04

23 lines
1494 bytes

I would like to know if anyone out there has experience in using the 
 Genesis Z-Tool, distributed by Imperial Software Technology (UK).
 We have been using  Version 2 (Jan 1992), and have
 encountered problems understanding the proof tool.   The main
problem is the connection between the syntax-directed editor  and the 
Common Lisp interface, and, especially, writing tactics in Lisp.

 If anyone can show us some worked examples of proofs using tactics,
 or point to any articles  or any other material which would help us
 understand this  proof tool,  it  would be greatly appreciated.
 
We have experience with both HOL and Isabelle, so understand the
general ideas and techniques involved in goal-directed proofs using tactics.


Thanks,

Dr Tony Cant
Trusted Computer Systems Group
Information Technology Division
Defence Science and Technology Organisation
SALISBURY South Australia
(cant@itd.dsto.gov.au)

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads