Computational logic systems, such as theorem provers and model checkers, produce evidence of a successful proof in an assortment of (often ad hoc) formats. Unfortunately, the evidence generated by one prover is seldom readable by another prover or even by a future version of itself. As a result, provers seldom trust and use proofs from other provers. This situation is made all the more regrettable given that logic and (formal) proof are certainly candidates for universally accepted standards. I will overview some recent work on designing a trustworthy proof checker that is able to check a range of proof structures (eg, natural deduction, resolution refutations, and proof nets) in classical, intuitionistic, and linear logics. I will also describe various future directions for this effort, including building marketplaces and libraries for proofs and developing ways to check and use partial proofs and counterexamples.
Takustr. 9, SR 005. Ab 13:45 Uhr Kaffee mit dem Vortragenden im Raum 137