Slides and Recordings for Presentations I Have Given

These are accumulated slides and recordings I have put together over the years, starting around 1990. Some are thus very old, out of date, have broken links, etc. I have put the most recent ones at the top of each section. Reports of errors, broken links, etc., will gratefully received.

Recordings

• Course at UM, August-December 2024: The whole course, see by topic at course content.
• Lectures at UNAL, November 2024: Overview, Practicum PRP,FOF, Practicum FOF,TFF, Principles, Practicum TXF,THF,NTF.

ATP General

• ATP
• A Chat with Bard
• Towards StarExec in the Cloud
• The Arrival of Automated Reasoning
• Larry Wos - Visions of Automated Reasoning

TPTP World

• The TPTP World - Infrastructure for Automated Reasoning
• Stepping Stones in the TPTP World
• The TPTP World Tutorial
• The TPTP Language for Writing Derivations and Finite Interpretations
• The TPTP Problem Library
• The TSTP Solution Library
• System on TPTP
• The SZS Ontologies for Automated Reasoning Software
• Specialist Problem Classes
• TSTP Standards
• The TPTP Process Instruction Language with Applications
• Tons of Data for Theorem Provers - The TDTP Data Library
• Thousands of Models for Theorem Provers - The TMTP Model Library
• Mathematics in the TPTP World

TPTP World Views

• From the TPTP to the TSTP - Problems and Solutions for Automated Theorem Proving
• TPTP-CASC-SSCPA - A Trilogy of Automated Theorem Proving Acronyms
• Standards and Tools for Component-based Automated Reasoning
• QED and the TPTP World
• The TPTP World - Infrastructure for Automated Reasoning
• The Expansion, Modernisation, and Future of the TPTP World
• The Future of the TPTP World

TPTP Logics

• The Logic Languages of the TPTP World
• Logic for PyRes
• Typed First-order Form
• TXF: The TPTP Typed Extended First-order Form
• Progress in the Development of Automated Theorem Proving for Higher-order Logic
• TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism
• The TPTP World of Non-classical Logics
• Solving QMLTP Problems by Translation to Higher-order Logic
• Proofs of Equivalence in Modal Logic Systems
• Automated Reasoning for the Dialetheic Logic RM3
• Making Belnap's "Useful 4-Valued Logic" Useful
• Description Logic Form
• Hoping for the Truth - A Survey of the TPTP Logics

TPTP Tools

• Semantic Derivation Verification
• AGMV - Semantic Model Verification
• GMV - Semantic Model Verification
• IDV - Interactive Derivation Viewer
• IIV - Interactive Interpretation Viewer
• The TPTP2T Problem and Solution Selector
• Automated Generation of Interesting Theorems
• Automatic Generation of Benchmark Problems for Automated Theorem Proving Systems
• Proving Hard Theorems in Rich Theories
• Proving Hard Theorems in Rich Theories, Part II
• Prophet - Prophesying Axiom Relevance by Symbol Overlap
• Multiple Answer Extraction for Question Answering with Automated Theorem Proving Systems
• Lemma Management Techniques for Automated Theorem Proving
• The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics

Evaluation

• The CADE ATP System Competition
• Things You Can't Do with a Vampire
• An Empirical Assessment of Progress in Automated Theorem Proving
• Progress in Automated Theorem Proving 1997 - 1999
• How Good is your Theorem Prover? (How Hard is that Problem?)
• Evaluating Automated Theorem Proving Systems (for CASC)
• Homogeneous Sets of ATP Problems

Proofs and Models

• Proofs and Models in the TPTP World
• Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
• TPTP World Standards and Tools for Tarskian and Kripke Interpretations
• Quality Metric for Proofs
• Combining Proofs to form Different Proofs
• Different Proofs are Good Proofs
• Presenting TSTP Proofs with Inference Web Tools

ATP Systems

• Smart Selective Competition Parallelism Automated Theorem Proving
• Compositional Competition-Cooperation Parallel Automated Theorem Proving
• JGXYZ - An ATP System for Gap and Glut Logics
• SRASS - A Semantic Relevance Axiom Selection System
• Divvy: An ATP Meta-system based on Axiom Relevance Ordering
• ATP by Reducing Axioms
• ATP by Binary Search Over Axiom Sets
• PTTP+GLiDeS - Semantically Guided PTTP
• GLiDeS' Models - Using Models to Guide Linear Deductions
• SPASS-XDB - Automated Reasoning with World Knowledge

TPTP Applications

• ATP Cross-Verification of the Mizar MPTP Challenge Problems
• Integration of the TPTPWorld into SigmaKEE
• Discrete Event Calculus Deduction using First-Order Automated Theorem Proving
• Why is Surface Area Important to Normal Cell Function?

Miscellaneous

• Ethical AI
• Computational Morality: Who Lives, Who Dies?
• SAMHT - Suicidal Avatars for Mental Health Training
• Projector Problem
• White Board