Křížová verifikace pomocí ATP mizarovské MPTP výzvy k řešení problémů

Abstrakt

tento článek popisuje, jak překlad z Mizaru do ATP (MPTP system), ATP verifikační systém (System GDV) a system Automatického Dokazovani Vět (ATP) byly společně použity pro nezávislou křížovou kontrolu části Mizarovy Matematické Knihovny (MML)

Klíčová slova

• Cross-Verification
• Mizar
• Challenge
• Problems