ATP, What is it Good For?

Mathematics

• Solving the Robbins Problem using EQP at ANL
• Euclidian geometry with Wu's Method
• New results in quasi-group theory using Mace at ANL
• Automated theory formation in mathematics with HR
• Cross-verification of the Mizar mathematical library at Charles University
• Equational theorem proving in Mathmatica
• Natural language proof checking with Naproche in Bonn

Software Creation and Verification

• Algorithm design, analysis, and optimization using KIDS at Kestrel
• Program synthesis at NASA
• Certifiable program synthesis at NASA
• Formal software specification and verification in the KeY Project
• Developing bug-free software at Escher Technologies
• Software verification using PVS at SRI
• Certifiable complex high assurance applications at Rockwell Collins
• Software analysis and verification at Microsoft
• Reliable software development and deployment by TRESOR

Hardware Creation and Verification

• Modeling computer systems using ACL2
• IC verification by JASPER
• Chip verification at Intel

Reasoning about Processes

• Formal analysis of security APIs in the SECSI project
• Process specification in PSL
• Verifying security protocols using Isabelle

Semantic and Knowledge-based Systems

• Semantic web service and process specification in Georgia
• Reasoning for the semantic web using Metalog or in REWERSE
• Natural language processing with DORIS
• Knowledge based reasoning in the Suggested Upper Merged Ontology
• Knowledge based reasoning in the Cyc Knowledge Base
• Deduction-based question answering using LogAnswer