Email Gateway (Aug 19 2022 at 10:38): Email Gateway (Aug 19 2022 at 10:38):From: Lars Hupel <hupel@in.tum.de>
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:
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
Email Gateway (Aug 19 2022 at 10:38):From: "Erwin R. Catesbeiana" <erwin@informatik.uni-bremen.de>
Dear list,
please find attached a related paper.
In particular, note my argument at the end of section 6 about Frege’s
Begriffsschrift.
All the best,
Erwin
paper.pdf
Email Gateway (Aug 19 2022 at 10:48):From: Peter Lammich <lammich@in.tum.de>
Hi Lars.
A really nice work. I do not want to use any other Isabelle-Logic any
more!
Here are some first impressions and suggestions for improvement:
1) I'm really missing sledgehammer. I have a problem to prove the
following theorem, which is an old challenge problem from a leading CPU
manufacturer:
theorem fpu_correct: "1.0 + 1.0 = 3.0"
Due to my understanding, the Falso-Logic should be able to prove it.
However, when I tried sledgehammer, it does not find a proof? Any hints?
2) For some really nasty Isabelle-Hacking, that I do not dare to
reproduce on this list, a lemma of the following form would be nice:
lemma: "PROP P"
However, my attempt to prove that "by exfalso" failed. Any chance to
extend the proof method such that it also proves this lemma?
Thanks again for this really great hack,
Peter
Email Gateway (Aug 19 2022 at 10:50):From: Brian Huffman <huffman@in.tum.de>
On Sun, Mar 31, 2013 at 4:52 PM, Peter Lammich <lammich@in.tum.de> wrote:
Hi Lars.
A really nice work. I do not want to use any other Isabelle-Logic any
more!
I agree! I've only used the new system for a few minutes, but it's
already immediately apparent what an improvement it is: For ease of
use, conciseness and elegance of proofs, there is no comparison.
Here are some first impressions and suggestions for improvement:
[...]
Even with the shortcomings that Peter has noted, I have already been
able to make great progress with the new system - even proving
original theorems that would have taken years (or decades!) of work
with the old Isabelle. For example:
theory P_is_NP
imports HOLF
begin
theorem P_is_NP: "P = NP"
by exfalso
end
Simply amazing!
Email Gateway (Aug 19 2022 at 10:51):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I thought I should maybe reply to these questions since it was me who
wrote most of exfalso:
1) I'm really missing sledgehammer. I have a problem to prove the
following theorem, which is an old challenge problem from a leading CPU
manufacturer:
theorem fpu_correct: "1.0 + 1.0 = 3.0"Due to my understanding, the Falso-Logic should be able to prove it.
However, when I tried sledgehammer, it does not find a proof? Any hints?
My intuition tells me that exfalso should work fine on propositions like
that; I cannot guarantee that it will always work, but in this instance,
it works fine. Personally, I think the possibilities of application of
the exfalso prover in circuit verification are virtually unlimited, but
I'm hardly an expert in this area.
The integration with sledgehammer is a known issue; remember, this is
still merely a prototype and we did not put too much effort into getting
it to work with Sledgehammer. I don't know where the problem is here,
but unlike some other projects, we actually have a bug tracker, so you
may want to file a bug report about this:
https://github.com/larsrh/hol-falso/issues
2) For some really nasty Isabelle-Hacking, that I do not dare to
reproduce on this list, a lemma of the following form would be nice:
lemma: "PROP P"
The purpose of the exfalso prover is mainly to extend and, in the long
run, replace certain older and somewhat slow and unreliable methods like
"blast" and "auto"; therefore, like these methods, it was not designed
to handle "prop" values. However, if you have an idea how to integrate
something like that into exfalso, do tell us, or better still, feel free
to fork the repository on Github and send us a pull request once you're
done.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 10:52):From: Alexander Krauss <krauss@in.tum.de>
Hi,
I also like this work, in particular the unifying approach towards the
notions of "True" and "False". Up to now, the community has been quite
dogmatic in this respect.
The new axiom can only prove valid statements of HOLF. However, your
lemma is a statement of Pure, but not HOLF. Embedding a powerful logic
in Pure does not make Pure itself more powerful. In fact, the statement
above is the single axiom of the even stronger system PureF, which can
prove all theorems of HOLF and many more...
Alex
Last updated: Apr 26 2024 at 12:28 UTC