[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?

Thanks again,
Reza.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.