Formalization of the Resolution Calculus for First-Order Logic

DOI10.1007/978-3-319-43144-4_21MaRDI QIDQ2829269zbMATH OpenOpenAlexFDO

Authors 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

resolutioncompletenessfirst-order logicHerbrand's theoremIsabelle/HOLsoundness

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)

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

Cites work

• scientific article; zbMATH DE number 1301853 (Why is no real title available?)
• scientific article; zbMATH DE number 976360 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Mathematical Logic for Computer Science
• On Different Concepts of Resolution
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• System description: E 1.8
• The Gödel completeness theorem for uncountable languages
• Theorem Proving in Higher Order Logics
• Towards Self-verification of HOL Light
• Unified Classical Logic Completeness

Cited in

(13)

• 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
• Formalized proof systems for propositional logic
• A verified SAT solver framework including optimization and partial valuations
• 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
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Programming and verifying a declarative first-order prover in Isabelle/HOL
• scientific article; zbMATH DE number 5173934 (Why is no real title available?)
• Formalizing a Seligman-style tableau system for hybrid logic (short paper)

Describes a project that uses

Uses Software

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

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)