ATP for the Novice

Ignorance at 3 Levels

• Logical consequence is ignorant of the meaning
• ATP systems are ignorant of the meaning
• ATP users can be ignorant of the meaning
  • This is the ignorance in focus

Styles of ATP Use

• Domain expert using ATP, e.g., Belinfante, Kunen
  • Success depends on domain expertise
  • Success illustrates benefits of ATP

• Domain novice using ATP, e.g., Wos, Sutcliffe
  • Success depends on ATP expertise
  • Success heralds the Arrival of ATP
  • Domain novice follows no preconceived approach