NetNews Usenet Archive 1992 #16/NN_1992_16.iso/spool/sci/math/symbolic/2087

Text File | 1992-07-27 | 8.8 KB | 270 lines

Newsgroups: sci.math.symbolic
Path: sparky!uunet!gatech!taco!eos.ncsu.edu!jwb
From: [e-mail] (Dr. John W. Baugh Jr.)
Subject: Re: sigma-algebras and probability spaces
Message-ID: <[e-mail]>
Sender: [e-mail] (USENET News System)
Reply-To: [e-mail]
Organization: North Carolina State University
References: <[e-mail]>
Date: Mon, 27 Jul 1992 17:39:45 GMT
Lines: 257

Harald Kirsch writes:

> Dear Netters,
>
> I am looking for a sw package that can do symbolic computations in
> $\sigma-$algebras (set theory). In the moment I have access only to
> Maple and it looks like it can not do what I need:

Try LP, the Larch Prover.  See the attached announcement and sample lp
file.

John Baugh
[e-mail]

-----

                 LP, The Larch Prover
                             --------------------

                  Release 2.2
                   November 27, 1991


     LP [1] is an interactive proof-assistant for a subset of multisorted
first-order logic.  It is designed to work efficiently on large problems and to
be used by relatively naive users.  Among its current uses are analyzing formal
specifications [2], reasoning about concurrent algorithms and hardware designs
[4,5], and proving theorems in algebra [3].

     LP's design is based on the assumption that initial attempts to state
conjectures correctly, and then prove them, usually fail.  As a result, LP is
designed to carry out routine (and possibly lengthy) steps in a proof
automatically and to provide useful information about why proofs fail, if and
when they do.  LP is not designed to find difficult proofs automatically;
instead, LP makes it easy for users to employ standard techniques such as
proofs by cases, induction, and contradiction.

     LP allows users to axiomatize theories by equations (i.e., quantifier-free
formulas), operator theories (e.g., commutativity), deduction rules (equivalent
to universal-existential formulas), and induction rules.  LP automatically
orients most equations into terminating rewrite rules, which it then uses in
equational term-rewriting to simplify axioms and conjectures.  LP automatically
applies deduction rules to derive consequences from newly asserted, simplified,
or proved equations and rewrite rules.

     LP can be obtained by anonymous ftp from larch.lcs.mit.edu (18.26.0.95).
You should use a dialog such as
     csh>>ftp larch.lcs.mit.edu
     Name: anonymous
     Password: <your name and location>
     ftp> cd pub/lp
     ftp> binary
     ftp> get lp2.2.lib.tar.Z
     ftp> get lp2.2.decmips.Z
     ftp> quit
to get the file lp2.2.lib.tar.Z (~420K), which contains documentation and a
runtime library for LP, together with one of the following compressed
executable versions of LP:
     lp2.2.decmips.Z    for DEC/MIPS 3100 or 5000 workstations (~1.1 meg)
     lp2.2.mips.Z    for MIPS workstations (~1.1 meg)
     lp2.2.sparc.Z    for Sun Sparcstations (~1.4 meg)
     lp2.2.sun3.Z    for Sun-3 workstations under Sun Unix 4.3 (~260K)
     lp2.2.vax.Z    for DEC VAX computers under Berkeley Unix 4.3 with NFS
            or a compatible version of Unix such as Ultrix (~260K)
To install LP, uncompress the executable file and install it as lp in
/usr/local/bin (or in any other directory on your search path).  Also, install
LP's runtime library by typing the following commands:
     uncompress lp.2.2.lib.tar.Z
     mkdir /usr/local/lib/lp
     mv lp.2.2.lib.tar.Z /usr/local/lib/lp
     cd /usr/local/lib/lp
     tar xf lp.2.2.lib.tar
If you cannot create /usr/local/lib/lp, you can install LP's runtime library in
some other directory and alias the the command "lp" to "lp -d directory-name".

     To run LP on some other machine (e.g., a Sony or Hewlett-Packard
workstation), or under some other operating system (e.g., Berkeley 4.2 Unix or
Berkeley 4.3 Unix without NFS), you should get the compressed tar file
lp2.2.code.tar.Z (~535K) containing source code, as well as lp2.2.lib.tar.Z,
and compile your own executables.

     To compile LP, you will need a CLU compiler and runtime system.  For VAX
and 68000 based architectures, these are available by anonymous ftp from
pion.lcs.mit.edu (18.26.0.64) in the directory pub/clu.  For other
architectures, such as the DEC/MIPS workstations and Sun Sparcstations, a
portable CLU compiler is available by anonymous ftp from mintaka.lcs.mit.edu
(18.26.0.36) in the directory pub/pclu.  If you use this implementation of CLU,
which translates CLU sources into C, you may also want to get the compressed
tar file lp2.2.c.tar.Z containing the C translations of the CLU sources
(getting these files saves the time required for retranslation).  See the file
INSTALLING in the distribution for information about compiling LP and about
overcoming installation problems.

     No license is required for using LP.  The file COPYRIGHT in the
distribution contains further information about using and redistributing LP.

     If you have problems with this distribution, or if you find bugs in LP,
please contact
     Stephen Garland
     MIT Laboratory for Computer Science
     545 Technology Square
     Cambridge, MA  02139
or send network mail to [e-mail].  If you decide to become a
user of LP, please send us mail at the above address, both so that we know who
our users are and so that we can mail you announcements of workshops, new
releases, and bug fixes.


References
----------

[1] S. J. Garland and J. V. Guttag.  A Guide to LP, The Larch Prover.  MIT
    Laboratory for Computer Science, December 1991.  Also available from DEC
    Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, as Report
    82.  A PostScript file containing this report is part of the distribution.

[2] S. J. Garland, J. V. Guttag, and J. J. Horning. "Debugging Larch Shared
    Language specifications," IEEE Transactions on Software Engineering 16:9
    (September 1990), pp. 1044-1057.  Also available as DEC Systems Research
    Center Report 60 (July 1990).

[3] U. Martin and M. Lai, "Some experiments with a completion theorem prover,"
    Journal of Symbolic Computation, to appear, 1991.

[4] J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning, "Using
    transformations and verification in circuit design," DEC Systems Research
    Center Report 78, September 1991.

[5] J. Staunstrup, S. J. Garland, and J. V. Guttag.  "Localized verification of
    circuit descriptions," Proc. Int. Workshop on Automatic Verification
    Methods for Finite State Systems, Grenoble, France, Lecture Notes in
    Computer Science 407, Springer-Verlag, 1989, pp. 349-364.

-----

% Proofs by induction of some properties of sets

clear
set log set
set script set
set trace 0

set name set

declare sorts Elem, Set
declare variables e, e': Elem, x, y, z: Set
declare operators
  empty:               -> Set
  insert:    Elem, Set -> Set
  singleton: Elem      -> Set
  \union:    Set, Set  -> Set
  \in:       Elem, Set -> Bool
  \subset:   Set, Set  -> Bool
  ..


% Axioms

assert Set generated by empty, insert
assert Set partitioned by \in
assert ac \union

assert
  singleton(e) == insert(e, empty)
  empty \union x == x
  insert(e, x) \union y == insert(e, x \union y)
  not(e \in empty)
  e \in insert(e', x) == e = e' | e \in x
  empty \subset x
  insert(e, x) \subset y == e \in y & x \subset y
  ..


% Theorems about union

set name theorem

prove e \in (x \union y) == e \in x | e \in y by induction on x
  qed

prove x == x \union x
  instantiate s1 by x, s2 by x \union x in deduction-rule
  qed

prove x == x \union empty
  instantiate s1 by x, s2 by x \union empty in deduction-rule
  qed



% Theorems about insert

prove insert(e, insert(e, x)) == insert(e, x)
  instantiate
    s1 by insert(e', insert(e', x)),
    s2 by insert(e', x)
    in deduction-rule
    ..
  qed

prove insert(e, x) == x \union singleton(e)
  qed



% Theorems about subset

prove (e \in x & x \subset y) => e \in y by induction on x
  resume by =>
    resume by case ec = e1c
    % Fast way to finish proof: instantiate e by ec, y by yc in inductHyp
    set immunity on
    critical-pairs *InductHyp with *ImpliesHyp
    set immunity off
    make nonimmune theorem
    critical-pairs *ImpliesHyp with theorem
    qed

prove insert(e, x) \subset y == e \in y & x \subset y
  qed

prove singleton(e) \subset x == e \in x
  qed

prove (x \union y) \subset z == x \subset z & y \subset z by induction on x
  qed


% Alternate induction rule

set name inductionRule

prove set generated by empty, singleton, \union
  resume by induction
  set name lemma
  critical-pairs *GenHyp with *GenHyp
  critical-pairs *InductHyp with lemma
  qed

set name theorem

prove x \subset (x \union y) by induction on x using inductionRule
  qed

prove x \subset x by induction using inductionRule
  qed

prove (x \subset y & y \subset z) => x \subset z
  resume by induction on x using inductionRule
    resume by =>
      critical-pairs *Hyp with *
  qed



display
statistics