Email Gateway (Aug 22 2022 at 21:12): Email Gateway (Aug 22 2022 at 21:12):From: Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Hi Peter,
well spotted. The proofs of one subgoal of that subclass statement and four lemmas further down have been generated automatically. I used Prover9 and wrote a simple translator to Isar.
More details: the classes implement algebras. The assumptions are axioms, which are manually encoded as input for Prover9 together with the statement you want to prove. Prover9 generates quite detailed output including a deduction if it finds a proof. It is mostly straight-forward to translate to Isar (outside of Isabelle) and usually metis can prove the individual steps. Sometimes a bit of manual post-processing was needed, such as using smt or Sledgehammer if metis failed to prove a step. Also the translator currently does not handle constants which appear in some Prover9 proofs. The method worked quite well for this kind of reasoning in algebras. I only used it when I could not make any progress using Sledgehammer.
Cheers,
Walter
Email Gateway (Aug 23 2022 at 08:17):From: Tobias Nipkow <nipkow@in.tum.de>
A Hierarchy of Algebras for Boolean Subsets
Walter Guttmann and Bernhard Möller
We present a collection of axiom systems for the construction of Boolean
subalgebras of larger overall algebras. The subalgebras are defined as the range
of a complement-like operation on a semilattice. This technique has been used,
for example, with the antidomain operation, dynamic negation and Stone algebras.
We present a common ground for these constructions based on a new equational
axiomatisation of Boolean algebras.
https://www.isa-afp.org/entries/Subset_Boolean_Algebras.html
Enjoy!
smime.p7s
Email Gateway (Aug 23 2022 at 08:17):From: Peter Lammich <lammich@in.tum.de>
Hello Walter and Bernhard
There seems to be some auto-generated proofs, e.g.
subclass boolean_algebra
proof
...
however, I don't know a tool that would generate proofs that look like
that? Are they actually auto-generated? What tool did you use?
Best,
Peter
Last updated: Apr 25 2024 at 04:18 UTC