Verifying a sequent calculus prover for first-order logic with functions in Isabelle/HOL

From MaRDI portal

Publication:6572548

Jump to:navigation, search

DOI10.4230/lipics.itp.2022.13MaRDI QIDQ6572548

Frederik Krogsdal Jacobsen, Asta Halkjær From

Publication date: 15 July 2024

zbMATH Keywords

completeness first-order logic soundness Isabelle/HOL prover SeCaV

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

This page was built for publication: Verifying a sequent calculus prover for first-order logic with functions in Isabelle/HOL

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:6572548&oldid=40111412"