A naive prover for first-order logic: a minimal example of analytic completeness

DOI10.1007/978-3-031-43513-3_25MaRDI QIDQ6541166zbMATH OpenFDO

Authors Asta Halkjær From, Jørgen Villadsen

Publication date 17 May 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-43513-3_25

zbMATH Keywords

completenessfirst-order logicIsabelle/HOLprover

Mathematics Subject Classification ID

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

Cites work

• Automated natural deduction in THINKER
• Concrete semantics. With Isabelle/HOL
• Die Vollständigkeit der Axiome des logischen Funktionenkalküls.
• Formalized proof systems for propositional logic
• Formalized soundness and completeness of epistemic logic
• scientific article; zbMATH DE number 1765709 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Mathematical Logic for Computer Science
• Programming and verifying a declarative first-order prover in Isabelle/HOL
• Soundness and completeness proofs by coinductive methods
• Teaching Automated Theorem Proving by Example: PyRes 1.2
• The Discovery of My Completeness Proofs
• Theorem Proving in Higher Order Logics
• Unified Classical Logic Completeness
• Verifying a sequent calculus prover for first-order logic with functions in Isabelle/HOL

This page was built for publication: A naive prover for first-order logic: a minimal example of analytic completeness

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6541166)