Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL.

Asta Halkjr From, Frederik Krogsdal Jacobsen

Browse the full ITP paper archive.