Introduction

My Background

• Classical logic, automated theorem proving (ATP)
• The TPTP and TSTP libraries
• CASC
• SPASS-XDB

My Mission

• Vinay's invitation
• The DKR Challenge
  • Exercising the new TFF capability in ATP
  • Using SUMO
• Generally, a classical logic approach