Some Impressive Achievements
In the classical 1st order, fully automatic, setting ...
Techniques
- Resolution
- Systems from ANL; "given clause" loop
- Paramodulation
- Subsumption
- Tableaux and Model Elimination
- Knuth-Bendix completion
- Indexing techniques
Implementations
- Otter
- Gandalf
- Vampire
- SPASS
- E
Solutions
- Robbins problem (EQP)
- Characterization of quasigroups (MGTP)
- Protocol verification (SPASS)
- Program synthesis (SNARK)