Formalization of the resolution calculus for first-order logic

DOI10.1007/s10817-017-9447-zzbMath1451.03019OpenAlexW2787858359MaRDI QIDQ1663242

Anders Schlichtkrull

Publication date: 21 August 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

completenessfirst-order logicresolutionsoundnessHerbrand's theoremIsabelle/HOLsemantic trees

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

On structures of regular standard contradictions in propositional logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Verified Decision Procedures for Modal Logics. ⋮ Unnamed Item ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover

Uses Software

• Isabelle
• Isabelle/HOL
• SPASS
• Isar
• Sledgehammer
• LCF
• Milawa
• E Theorem Prover
• Jitawa
• IsaFoL
• theoremprover-museum
• GRAT
• GitHub
• Completeness theorem
• Superposition Calculus
• Paraconsistency
• Knuth Bendix Orders
• Abstract Completeness
• FOL Fitting
• Incompleteness Theorems
• Archive Formal Proofs
• Lambda Free RPOs
• Verified Prover
• Abstract Soundness
• Incredible Proof Machine
• Propositional Resolution
• FOL_Harrison

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Kripke models for classical logic
• Formal correctness of a quadratic unification algorithm
• Partial and nested recursive function definitions in higher-order logic
• Verifying the unification algorithm in LCF
• Deductive synthesis of the unification algorithm
• Isabelle/HOL. A proof assistant for higher-order logic
• Extending Sledgehammer with SMT solvers
• Soundness and completeness proofs by coinductive methods
• A transfinite Knuth-Bendix order for lambda-free higher-order terms
• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
• 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
• System Description: E 1.8
• Truly Modular (Co)datatypes for Isabelle/HOL
• Mathematical Logic for Computer Science
• Concrete Semantics
• A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
• Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
• Foundational extensible corecursion: a proof assistant perspective
• Unified Classical Logic Completeness
• Towards Self-verification of HOL Light
• On Different Concepts of Resolution
• Metamathematics, Machines and Gödel's Proof
• Term Rewriting and All That
• The Blossom of Finite Semantic Trees
• Theorem Proving in Higher Order Logics
• A Machine-Oriented Logic Based on the Resolution Principle
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Efficient verified (UN)SAT certificate checking

This page was built for publication: Formalization of the resolution calculus for first-order logic