Other Mathematics Commons^™

Automated Theorem Prover Axiom Management, Ashley T. Holeman, Ewen Denney

STAR Program Research Presentations

Automated Theorem Provers (ATPs), are computer programs that use collections of axioms,which are logical statements assumed to be true, in order to prove conjectures. NASA uses these programs to verify safety and functional requirements in domains like Guidance, Navigation, and Control. There are about 30 axioms on each major topic including the theory of coordinate systems, elementary arithmetic and linear algebra. These axioms have been created over the duration of many projects and combined into a single file. One task is to manage the axioms by arranging them into logical sections, deleting unnecessary ones and rewriting some into a more …