Formalization of the resolution calculus for first-order logic

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

Cites Work

Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
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
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
Theorem Proving in Higher Order Logics
Term indexing
Partial and nested recursive function definitions in higher-order logic
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
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 (11)

Title not available (Why is that?)
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

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)