Programming and verifying a declarative first-order prover in Isabelle/HOL

DOI10.3233/AIC-180764zbMath1462.68214OpenAlexW2797950816MaRDI QIDQ5145439

Jørgen Villadsen, Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull

Publication date: 20 January 2021

Published in: AI Communications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3233/aic-180764

zbMATH Keywords

verificationsoundnessIsabelledeclarative proofs for first-order logic with equalityLCF-style prover

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• Isar
• HOL
• Isabelle/jEdit
• Sledgehammer
• Metamath
• GitHub
• Completeness theorem
• Superposition Calculus
• FOL Fitting
• Archive Formal Proofs
• Verified Prover
• FOL_Harrison

Cites Work

• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• How to write a 21\(^{\text{st}}\) century proof
• Proof assistants: history, ideas and future
• Seventy-five problems for testing automatic theorem provers
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• Soundness and completeness proofs by coinductive methods
• Visual Theorem Proving with the Incredible Proof Machine
• Formalization of the Resolution Calculus for First-Order Logic
• The Gödel Completeness Theorem for Uncountable Languages
• Code Generation via Higher-Order Rewrite Systems
• Towards Self-verification of HOL Light
• How to Write a Proof
• Extending Sledgehammer with SMT Solvers
• Theorem Proving in Higher Order Logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Programming and verifying a declarative first-order prover in Isabelle/HOL