MPTP - Motivace, implementace, první experimenty

Abstrakt

Popis systému MPTP, který překládá matematickou knihovnu Mizar pro automatické dokazovače pracující v logice prvního řádu.

Klíčová slova

• Motivation
• Implementation
• First
• Experiments