Proving New Theorems

• Combine the Proof Advisor with ATPs to attempt fully automated theorem proving over MML
• Evaluation: For each MML theorem T, use the Advisor hints from incremental training on previous MML for ATPs, to attempt the proof of T
• About every seventh MML theorem can thus be proved for MPTP 0.1.
• About every fifth nonnumerical theorem can thus be proved for MPTP 0.2.
• The ATP proofs are sometimes completely different from the MML proofs - proof discovery and improvement

Table 1: Proving New Theorems in MPTP 0.1. (SPASS)

proved	completion found	timeout	out of memory	unknown	total
4825	7	28580	69	46	33527

Table 2: Proving new (nonnumerical) theorems with machine learning support in MPTP 0.2.

description	proved	countersatisfiability	timeout or memory out	total
E 0.9	2167	0	10362	12529
SPASS 2.1	1543	0	10986	12529
together	2408	0	10121	12529