[isabelle] Announcement: Isabelle/HOLF



Dear list,

in 2011, Amarilli (at the time working at Estatis, Inc.) et al. shook
the very foundations of mathematics and logics with the introduction of
Falso [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.

In an attempt to integrate this powerful new approach with existing
formal proofs, we, the Theorem Proving Group at the FU Dietersheim,
extended the Isabelle/HOL system to Isabelle/HOLF, 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, exfalso,
which shows promising results so far, e.g. in proving the Riemann
conjecture (publication pending).

The key features of the Isabelle/HOLF axiom system and the corresponding
new proof methods are:

* Generally shorter, more readable proofs
* Highly parallelisable
* 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.)

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 Falso 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.

You can download a prototype of Isabelle/HOLF that integrates seamlessly
with Isabelle/HOL at our website [3]. If you wish, you can follow the
development at GitHub [4].

Happy experimenting
Lars Hupel


[1] Amarilli, A. 2011. Are You Using the Right Axiomatic System?
[2] Hupel, L. 2012. On the Integration of Falso with Existing Logical
Systems. Proceedings of the 2012 Dietersheim Weißwurstfrühstück.
[3] http://www.fu-dietersheim.de/logik/isabelle/holf/index.htm
[4] https://github.com/larsrh/hol-falso





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.