Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: info-hol@edu.uidaho.cs.ted
Subject: hol90 version 5 news
Message-Id: <93Mar13.180012met.8116@sunbroy14.informatik.tu-muenchen.de>
Date: Sat, 13 Mar 1993 18:00:05 +0100


The hol90 Version 5 News.


* New libraries.

The libraries "arith", "reduce", "unity", "abs_theory", "pred_set", and
"prog_logic" have been ported to hol90.


- Thanks to KimDam Peterson and Richard Boulton, the "reduce" and "arith" 
  libraries are now available. The former provides "symbolic computation" for 
  {bool,num} terms, and the latter provides a partial decision procedure for 
  Presburger arithmetic. (Legend has it that Tarski wouldn't give Presburger
  a thesis for his work, thinking it was a trivial application of 
  quantifier elimination. Also of note - the "thesis" was only 11 pages.)


- The "pred_set" library is now available. This is a close duplicate of the
  library of sets.


- Phil Windley's "abs_theory" library is now available, thanks to David
  Shepherd. Some improvements have been made over the original; an abstract
  theory is easier to declare, plus there is a body of specialized
  rewriting tools available for abstract theories. An example in the 
  sources shows the development of an abstract theory of monoids, and 
  from that, an abstract theory of groups.


- Flemming Anderson's formalization of Chandy and Misra's "unity" theory 
  is now available, thanks to KimDam Peterson and Flemming. Worked examples
  include dining philosophers, readers and writers, and an arbiter.


- Mike Gordon's "prog_logic" theory is now available, thanks to
  Matthew Morley. This provides Hoare logics for partial and total
  correctness plus a logic for Dijkstra's weakest preconditions and
  weakest liberal preconditions.


* New contrib additions.

- The "mutrec" library provides the ability to define mutually recursive
  types, and mutually recursive functions over those types. This library 
  is based on work by Elsa Gunter and Myra VanInwegen. The "example.sml" 
  file in contrib/mutrec shows the definition of the abstract syntax of a 
  small ML-like language, plus the definition of a mutually recursive 
  function over that syntax.


- Paul Loewenstein's automata theory, which addresses automata with 
  infinite state spaces. This work includes several versions of
  Koenig's Lemma. 


* New tools.

Thanks to Matthew Morley, "xholhelp" has been modified to work with
hol90. Its source can be found in the "tools" directory. 


* Miscellaneous.

The installation procedure has been simplified. There are some bugfixes
and additions, all noted in the file doc/4.changes.