Formalization of the Resolution Calculus for First-Order Logic
From MaRDI portal
Publication:2829269
DOI10.1007/978-3-319-43144-4_21zbMath1478.68442OpenAlexW2494829073MaRDI QIDQ2829269
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
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
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
