Formalization of the Resolution Calculus for First-Order Logic

DOI10.1007/978-3-319-43144-4_21zbMath1478.68442OpenAlexW2494829073MaRDI QIDQ2829269

Anders Schlichtkrull

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://backend.orbit.dtu.dk/ws/files/126069253/typeinst.pdf

zbMATH Keywords

completenessfirst-order logicresolutionsoundnessHerbrand's theoremIsabelle/HOL

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (7)

Soundness and completeness proofs by coinductive methods ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalization of the resolution calculus for first-order logic ⋮ Formalising Mathematics in Simple Type Theory ⋮ Unnamed Item ⋮ Programming and verifying a declarative first-order prover in Isabelle/HOL ⋮ Formalizing a Seligman-style tableau system for hybrid logic (short paper)

Uses Software

• Isabelle
• Isabelle/HOL
• SPASS
• HOL
• HOL Light
• IsaFoL
• Completeness theorem
• FOL Fitting
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• The Gödel Completeness Theorem for Uncountable Languages
• System Description: E 1.8
• Mathematical Logic for Computer Science
• Unified Classical Logic Completeness
• Towards Self-verification of HOL Light
• On Different Concepts of Resolution
• Theorem Proving in Higher Order Logics
• A Machine-Oriented Logic Based on the Resolution Principle
• Formalizing Bachmair and Ganzinger's ordered resolution prover

This page was built for publication: Formalization of the Resolution Calculus for First-Order Logic