-
Notifications
You must be signed in to change notification settings - Fork 1
/
01042013_presse_holf.html
47 lines (37 loc) · 2.3 KB
/
01042013_presse_holf.html
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
<body BGCOLOR=#ababab>
<h1>FUD Press Releases/Pressemitteilungen der FUD</h1>
<a name="falso">
<h2>Announcing Isabelle/HOLF</h2>
<p>1 April 2013
<code>
<p>In 2011, Amarilli (at the time working at Estatis, Inc.) et al. shook the very
foundations of mathematics and logics with the introduction of <i>Falso</i>
[1], a novel system of axioms that surpasses the ageing systems ZF and HOL in
many respects. In particular, it was shown that Falso can prove its own
consistency and allows for efficient implementation of theorem checkers and
proof assistants.
<p>In an attempt to integrate this powerful new approach with existing formal
proofs, we, the theorem proving group at the FU Dietersheim, extended the
<i>Isabelle/HOL</i> system to <i>Isabelle/HOLF</i>, which uses a hybrid version
of HOL and the original version of Falso [1]. In particular, we provide an
experimental amortised constant-time proof method, <i>exfalso</i>, which shows
promising results so far, e.g. in proving the Riemann conjecture (publication
pending).
<p>The key features of the Isabelle/HOLF axiom system and the corresponding new proof methods are:
<ul>
<li>Generally shorter, more readable proofs
<li>Highly parallelisable
<li>Fully backwards-compatible, i.e. legacy Isabelle/HOL proofs can be used with the new system without restrictions (An automatic conversion tool is in development.)
</ul>
<p>It has been noted critically that the introduction of new axioms is imprudent,
however, we argue that as the above results show, the benefit clearly outweighs
any of these objections. Additionally, it has been conjectured by [2] that the
addition of the <i>Falso</i> axioms may render a number of axioms in ZF and HOL
superfluous, which would lead to an axiom system that is both more powerful and
has fewer axioms than ZF and HOL, which is a clear indicator for robustness.
<p>You can download a prototype of Isabelle/HOLF that integrates seamlessly with
Isabelle/HOL <a href="logik/isabelle/holf">at our website</a>. If you wish, you
can follow the development at <a href="https://github.com/larsrh/hol-falso">GitHub</a>.
<p>[1] Amarilli, A. 2011. <i>Are You Using the Right Axiomatic System?</i>
<br>[2] Hupel, L. 2012. <i>On the Integration of Falso with Existing Logical Systems</i>. Proceedings of the 2012 Dietersheim Weißwurstfrühstück.
</pre>