And a nice April 1st for you too :-) On Apr 1, 2013 10:57 PM, "Valeria de Paiva" <[email protected]> wrote:
> 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 > > _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
