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

DOI10.1007/s10817-024-09697-3MaRDI QIDQ6611963

Asta Halkjær From, Frederik Krogsdal Jacobsen

Publication date: 27 September 2024

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

first-order logicsoundnessIsabelle/HOLCompletenessProverSeCaV

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