We believe that first order automation is useful in practice,
even in verification applications (floating point verification), and in
science - support for working mathematicians (data base of computer
checked mathematics). We can consider, that the attraction of FTP is
enhanced by co-locating with suitable events - such as CADE and Tableaux.
I would like to promote academic activities on first order theorem
proving in specialized domains, where systems need incorporate mathematical
knowledge. The FTP community should be more interested about applications
in education of mathematics, in order to have
more impact on the world.
Connection with FTP Workshops:
- FTP'98, Vienna, chairman of the session "Verification and Interpretation",
- IJCAR 2001, Siena, referee and PC of the Workshop 9.