Email Gateway (Aug 19 2022 at 11:02): 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: Nov 21 2024 at 12:39 UTC