Formalization of the Resolution Calculus for First-Order Logic
DOI10.1007/978-3-319-43144-4_21zbMATH Open1478.68442OpenAlexW2494829073MaRDI QIDQ2829269FDOQ2829269
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
Recommendations
- Formalization of the resolution calculus for first-order logic
- Resolution calculus for the first order linear logic
- Resolution approximation of first-order logics
- A resolution calculus for first-order schemata
- A resolution framework for finitely-valued first-order logics
- Resolution calculi for modal logics
- scientific article; zbMATH DE number 4055570
- scientific article; zbMATH DE number 4027426
- First-order resolution methods for modal logics
- scientific article; zbMATH DE number 1324435
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)
Cites Work
- System Description: E 1.8
- A Machine-Oriented Logic Based on the Resolution Principle
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Towards Self-verification of HOL Light
- Theorem Proving in Higher Order Logics
- Title not available (Why is that?)
- Title not available (Why is that?)
- On Different Concepts of Resolution
- Title not available (Why is that?)
- The Gödel completeness theorem for uncountable languages
- Mathematical Logic for Computer Science
- Unified Classical Logic Completeness
- Formalizing Bachmair and Ganzinger's ordered resolution prover
Cited In (11)
- A full formalization of SLD-resolution in the calculus of inductive constructions
- Formalization of the resolution calculus for first-order logic
- Formalising Mathematics in Simple Type Theory
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Soundness and completeness proofs by coinductive methods
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formalizing a Seligman-style tableau system for hybrid logic (short paper)
Uses Software
This page was built for publication: Formalization of the Resolution Calculus for First-Order Logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829269)
