Conclusion

Proof Dependence

• A new notion, extending axiom dependence
• Demodulation to junk as a methodology

BCSK Logic

• Two axioms shown to be dependent
• Three axioms shown to be proof dependent
• Third axiom shown to be dependent in extended logics

Ignorance and ATP

• Ignorance of the domain of application
  • 3 levels: logical consequence, ATP systems, ATP user
  • Does not deny success
  • May even be an advantage
• Ignorance at a 4th level
  • The paper presenter ... who will now try to answer questions