Cited in
(26)- A verified SAT solver framework with learn, forget, restart, and incrementality
- Unified Classical Logic Completeness
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- THINKER
- MUSCADET
- PVSio
- Formalization of the Resolution Calculus for First-Order Logic
- IsaFoL
- DPT
- Abstract Completeness
- FOL Fitting
- Abstract Soundness
- Incompleteness Theorems
- Paraconsistency
- NASA PVS
- Propositional Resolution
- SAT Solver Verification
- Superposition Calculus
- Verified Prover
- FOL_Harrison
- PyRes
- Formalization of the resolution calculus for first-order logic
- Formally verified tableau-based reasoners for a description logic
- Soundness and completeness proofs by coinductive methods
- Epistemic Logic
This page was built for software: Completeness theorem
