Message: 1 Date: Mon, 01 Apr 2013 00:03:06 +0200 From: Lars Hupel <[email protected]> Subject: [isabelle] Announcement: Isabelle/HOLF To: [email protected] Message-ID: <[email protected]> Content-Type: text/plain; charset=ISO-8859-15
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 -- Valeria de Paiva http://www.cs.bham.ac.uk/~vdp/ http://valeriadepaiva.org/ _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
