The TPTP World Tutorial

Introduction

• A Motivating Example
• ATP, What is it?
• ATP, What is it Good For?
• Another Motivating Example

Examples for the Education Process

• Propositional Logic
• First-order Logic
• Typed First-order Logic
• Typed Higher-order Logic

The ATP Process

• The Process Flowchart
• Examples for Practice (click)
  • A Theorem with Nice Axioms
  • A Non-Theorem with Nice Axioms
  • A Theorem with Nasty Axioms
• A Challenge Theorem

Ethics, Law, Medicine, Politics ...

• Explaining neural networks - Explainable AI
• Encoding the world - Ontologies
• Automating ethical decisions - The Moral Machine
• Formalizing religion - The Ontological Argument
• All need more expressive logics (click)
  • eXtended logics
  • More truth values
  • Modalities, e.g., Modal, Deontic, Dynamic, ... logics.

Automated Reasoning requires Intelligence

• Throw away (apparently) unnecessary axioms
• Do the (apparently) right inferences
• Explain the proof/counterexample to people

The End - Any Questions?