← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/ivy/ivy-v2/README

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/ivy/ivy-v2/README
 
1
===========================================================
 
2
Ivy: A Preprocessor and Proof Checker for First-order Logic
 
3
===========================================================
 
4
 
 
5
Files:
 
6
 
 
7
    README
 
8
    Configure
 
9
 
 
10
Subdirectories:
 
11
 
 
12
    ivy-sources
 
13
    otter-3.0.6     : the full otter-3.0.6 distribution
 
14
    mace-1.3.4      : the full mace-1.3.4 distribution
 
15
 
 
16
[Modification for ACL2 distribution:  To create directories otter-3.0.6 and
 
17
 mace-1.3.4 on your system, issue the following commands:
 
18
 
 
19
 gunzip otter-3.0.6.tar.gz
 
20
 tar xvf otter-3.0.6.tar
 
21
 rm otter-3.0.6.tar
 
22
 gunzip mace-1.3.4.tar.gz
 
23
 tar xvf mace-1.3.4.tar
 
24
 rm mace-1.3.4.tar
 
25
]
 
26
 
 
27
------------
 
28
INTRODUCTION
 
29
------------
 
30
 
 
31
Ivy is a preprocessor and proof checker for resolution/paramodulation
 
32
theorem provers.  It is coded in ACL2 and proved sound for finite
 
33
interpretations.
 
34
 
 
35
Ivy is described in a paper that will appear as a chapter in
 
36
        Computer-Aided Reasoning: ACL2 Case Studies
 
37
        -------------------------------------------
 
38
edited by Matt Kaufmann, Pete Manolios, and J Moore,
 
39
to be published by Kluwer Academic in 2000. See
 
40
http://www.wkap.nl/series.htm/ADFM.
 
41
 
 
42
The Ivy web page is http://www.mcs.anl.gov/~mccune/acl2/ivy.
 
43
 
 
44
----------
 
45
INSTALLING
 
46
----------
 
47
 
 
48
To install Ivy, you have to (1) run the Configure script to update
 
49
pathnames in several scripts, (2) certify the Ivy books, and
 
50
(3) compile the external programs Otter and MACE (this can
 
51
be done before running the Configure script if you like).
 
52
 
 
53
If all goes according to plan, the following commands should work.
 
54
(This works for us with ACL2-v2.4 on Linux and on Solaris.  The
 
55
three makes---Ivy, Otter, and MACE---are independent and can be
 
56
done in any order.)
 
57
 
 
58
 
 
59
    ./Configure  # this will ask some questions; try the default answers
 
60
 
 
61
    # Part 1. Make Ivy.
 
62
 
 
63
    [look at ivy-sources/arithmetic.lisp, and change the pathname if necessary]
 
64
    cd ivy-sources
 
65
    make &                       # 90 minutes, 21 megabytes of output
 
66
    cd ..
 
67
 
 
68
    # Part 2. Make Otter.
 
69
 
 
70
    cd otter-3.0.6/source
 
71
    make
 
72
    cd ../..
 
73
 
 
74
    # Part 3. Make MACE.
 
75
 
 
76
    cd mace-1.3.4
 
77
    make
 
78
    cd ..
 
79
 
 
80
    # Simple tests of Ivy; the first calls Otter, the second calls MACE
 
81
 
 
82
    ivy-sources/util/ivy  prove  ivy-sources/test/p-implies-p
 
83
    ivy-sources/util/ivy  model  ivy-sources/test/p
 
84
 
 
85
-------
 
86
RUNNING
 
87
-------
 
88
 
 
89
The ivy script in ivy-sources/util is the way to run Ivy.
 
90
The first argument is ( prove | refute | disprove | model ), and
 
91
the second argument is a file containing a formula.
 
92
You should be able to run it from anywhere, but you must have
 
93
write-permission in the directory containing the input file.
 
94
 
 
95
For further tests, see the README files in ivy-sources/test
 
96
and ivy-sources/examples.
 
97
 
 
98
---------
 
99
SAVED_IVY
 
100
---------
 
101
 
 
102
Running ivy-sources/util/ivy loads all of the Ivy books, which takes
 
103
a while.  Instead, you can try to create a saved_ivy file with the
 
104
command
 
105
 
 
106
    ivy-sources/util/make-saved-ivy
 
107
 
 
108
After several minutes, you should have a file ivy-sources/saved_ivy.
 
109
This seems to build a good saved_ivy on our Solaris systems, BUT IT
 
110
DOESN'T WORK ON OUR LINUX SYSTEMS.
 
111
 
 
112
You can run saved_ivy by using util/sivy instead of util/ivy:
 
113
 
 
114
    ivy-sources/util/sivy  prove  ivy-sources/test/p-implies-p
 
115
    ivy-sources/util/sivy  model  ivy-sources/test/p
 
116
 
 
117
William McCune (mccune@mcs.anl.gov, http://www.mcs.anl.gov/~mccune)
 
118
Olga Shumsky (shumsky@ece.nwu.edu, http://www.ece.nwu.edu/~shumsky)
 
119
 
 
120
April 2000