Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <24099-0@swan.cl.cam.ac.uk>; Sat, 29 Feb 1992 18:48:34 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13213; Sat, 29 Feb 92 10:36:30 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from acquine.cns.caltech.edu by ted.cs.uidaho.edu (16.6/1.34) id AA13167; Sat, 29 Feb 92 10:36:23 -0800 Received: from kafka.cns.caltech.edu by cns.caltech.edu (4.1/1.34) id AA05064; Sat, 29 Feb 92 10:36:07 PST Date: Sat, 29 Feb 92 10:36:07 PST From: kprasad@edu.caltech.cns (K. Prasad) Message-Id: <9202291836.AA05064@cns.caltech.edu> To: info-hol@edu.uidaho.cs.ted, nqthm-user@com.cli Subject: HOL, Boyer-Moore or Stateharts Am posting this for a friend. Thanks for any comments. +++ ----8<--------8<--------8<--------8<--------8<--------8<-------- I have a few requirement specifications that are expressed as Statecharts. I am interested in knowing if HOL or the Boyer-Moore logic gives me any more functionality than Statecharts. For example, what value would I get if I migrated from Statecharts to using one of these theorem provers? Can I reason about the specifications better and make them more complete? Right now, I feel that my specifications are "sort of" incomplete. Thanks in advance.