Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] fully automated methods(superposition etc.)

Email Gateway (Aug 19 2022 at 11:02):

From: Reza Roboubi <rezarob@gmail.com>
It worked like a charm, thanks.

Are techniques used by fully automated systems(like the E-prover and
superposition) applicable to human-assisted systems, or do they not
really fit well with the kinds of proofs humans produce?

For example, in IsarMathLib there is a lemma, "A trivial fact:identity
is the only function from a singleton to itself," where it appears
that humans still have to type several lines of proof to get something
trivial. Could "fully automated" techniques/systems simplify that?

Thanks again,
Reza.

Last updated: Apr 19 2024 at 12:27 UTC