Work in Progress

Derivations and Interpretations

• Dependently typed higher-order logic
• Derivation verification with LambdaPi
• Representation of clausal connection tableau proofs.
• Dealing with "gifts from God"
• New format for finite and infinite interpretations

StarExec

• In the AWS Cloud
• Containerised ATP systems (in general)

Reasoning in Reality

• ATP is NOT just verification
  • Encoding the world - Ontologies
  • Political argumentation - The CRAP Project
  • Automating ethical decisions - The Moral Machine
  • Formalizing religion - The Ontological Argument
  • Testing Public Policy
  • Explainable AI, Trustworthy AI, Verified AI
• More expressive logics
  • More truth values
  • Modalities, e.g., Modal, Deontic, Epistemic, Dynamic, ... logics.
• Reasoning in real-time, updating axioms (student needed)
• Answer Extraction

CASC and ProoVer

• CASC will run at CADE
• CASKet, with the ICV division, will run at IJCAR
• ProoVer will run at IJCAR
  • The IJCAR Proof Verification Competition
  • With Julie Callier and Simon Guilloud
  • Technical matters to be resolved
• Proofs will be verified