Proof Verification with GDV and LambdaPi
It's a Matter of Trust

• Status vs. Artifact
• Trust a tool(chain) to produce a correct status/artifact
• Trust a particular status/artifact
• Add trust to an untrustworthy tool

• When?
  • During system development
  • During system use
  • When it's worth waiting
• How?
  • Theoretical notions, Trustworthy cores
  • Empirical process

• What is Automated Reasoning?
• The TPTP World
• Bugs are a Reality
• Empirical process

• A Language
• A Proof format
• The SZS Ontologies

• Contributions
  • Clarity of Process
  • Implementation of GDV-LP

• Current
  • Proof format for clausal connection tableau, verification in GDV
  • Tarskian and Kripke model formats, verification in AGMV
  • ProoVer competition

• Future
  • Verifying subsymbolic systems
  • Verification of interferences, e.g., Skolemization
  • Modalities of trust, Probabilities of trust

The End - Any Questions?