Formalization of the resolution calculus for first-order logic

DOI10.1007/S10817-017-9447-ZzbMATH Open1451.03019OpenAlexW2787858359MaRDI QIDQ1663242FDOQ1663242

Authors: 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

Recommendations

• Formalization of the Resolution Calculus for First-Order Logic
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• A full formalization of SLD-resolution in the calculus of inductive constructions
• Theorem Proving in Higher Order Logics

zbMATH Keywords

resolutioncompletenessfirst-order logicHerbrand's theoremIsabelle/HOLsoundnesssemantic trees

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (12)

• Title not available (Why is that?)
• A full formalization of SLD-resolution in the calculus of inductive constructions
• On structures of regular standard contradictions in propositional logic
• Title not available (Why is that?)
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL
• Formalization of the Resolution Calculus for First-Order Logic
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Title not available (Why is that?)
• Title not available (Why is that?)
• Verified Decision Procedures for Modal Logics.

Uses Software

• Isabelle
• Isabelle/HOL
• SPASS
• Isar
• Sledgehammer
• LCF
• Milawa
• E Theorem Prover
• Jitawa
• IsaFoL
• theoremprover-museum
• GRAT
• 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
• GitHub

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 Q1663242)