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?