ATP, What is it Good For?

Mathematics

• Solving the Robbins Problem using EQP at ANL
• Euclidian geometry with Wu's Method
• New resuts for loops with Abelian inner mapping groups using Otter and hints
• Cross-verification of the Mizar mathematical library at Charles University
• Equational theorem proving in Mathmatica

Software Creation and Verification

• Certifiable program synthesis at NASA
• Formal software specification and verification in the KeY Project
• Developing bug-free software at Escher Technologies
• Software analysis and verification at Microsoft
• Software verification and certification at Imandra
• The Sledgehammer in Isabelle

Hardware Creation and Verification

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

Reasoning about Processes

• Process specification in PSL
• Verifying security protocols using Isabelle
• Provable security at Amazon

Semantic and Knowledge-based Systems

• Reasoning for the semantic web using Metalog or in REWERSE
• Knowledge based reasoning in the Suggested Upper Merged Ontology
• Deduction-based question answering using LogAnswer
• Reasoning about the world in the Singularity NET
• Winning Jeopardy!

The Real and Unreal World

• Legal reasoning in Luxembourg
• Consistent, Rational Arguments in Politics in the CRAP project
• Verification of voting by DemTech
• GDPR compliance at Signatu
• Proving the existence of God (the Ontological argument)