-
Notifications
You must be signed in to change notification settings - Fork 0
/
README
79 lines (52 loc) · 2.44 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
Isabelle/HOLF
Isabelle/HOL with Falso
Theorem Proving Group at FU Dietersheim
<http://www.fu-dietersheim.de/logik/isabelle/holf/>
Version information
Version: 1 April 2013
Isabelle/HOLF is still a prototype. Use at own risk!
This version of Isabelle/HOL has been tested with Isabelle/2013,
but it should be compatible with earlier versions of Isabelle as
well.
Installation
1. Extract the file HOLF.thy to the directory src/HOL/ of your
Isabelle installation.
2. Apply the patch Main.thy.diff in the "src/HOL/" directory,
i.e. export Main.thy.diff to some directory (e.g. /tmp/) and
run "patch < /path/to/difffile/Main.thy.diff" in the src/HOL
directory.
3. Rebuild your HOL heap image by running
"bin/isabelle build -b HOL"
You can then use the Falso axioms and the exfalso prover in your
theories.
Alternatively, if you do not want to alter your existing Isabelle
installation, you can also simply manually import the HOLF.thy
file in any of your Isabelle/HOL theories with the same effect.
Examples
In this tarball, you can also find the theory Fermat.thy, which
illustrates the usage of the HOLF system and the exfalso prover
on the example of the Fermat-Wiles Theorem, also known as
Fermat's Last Theorem.
Contrary to Fermat's original proof (if indeed he even had one),
this proof would comfortably fit into any margin.
Bug Reporting
HOLF is still in the early stages of its development and may
therefore still be somewhat unstable. Please report any bugs that
you find at our bug tracker:
<https://github.com/larsrh/hol-falso/issues>
In case you don't have a GitHub account, feel free to contact the
authors directly via mail:
Manuel Eberl <[email protected]>
Lars Hupel <[email protected]>
Snail mail contact
Fakultaet für Informatik
Freie Universitaet Dietersheim
Satiergartenstr. 42
D-85386 Dietersheim/Eching
Germany
__________________________________________________________________
Please report any problems you encounter. While we shall try to
be helpful, we can accept no responsibility for the deficiencies
of Isabelle, Isabelle/HOL, or your capacity for satire and their
consequences.
_________________________________________________________________