External Sources of Axioms in Automated Theorem Proving

Abstract

Automatic Theorem Proving (ATP) problems in large theories often have more axioms than can be effectively handled in memory. This work adresses the issues of accessing external sources of axioms from a first-order logic ATP system.

Keywords

• External
• Sources
• Axioms
• Automated
• Theorem
• Proving