[isabelle] fully automated methods(superposition etc.)
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and