Work in Progress

Derivations and Interpretations

• Standardization of derivations
• Derivation verification with LambdaPi
• Representation of clausal connection tableau proofs.
• Datatypes and Codatatypes
• A format for finite and infinite interpretations

StarExec

• StarExec in Kubernetes
• Containerised ATP system execution

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

• ProoVer verifier competition
• Proofs will be verified