Work in Progress

Derivations and Interpretations

• Propogate the new format for finite and infinite interpretations
• Derivation verification with LambdaPi
• Representation of other proof forms, e.g., tableau, sequent, and connection calculi (work!)
• IIV for Kripke interpretations (student needed)

StarExec in the Cloud

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 vs. ProoVer

• CASC will run at CADE
• ProoVer will run at IJCAR
  • The IJCAR Proof Verification Competition
  • With Julie Callier and Simon Guilloud
  • Technical matters to be resolved