Superposition Calculus
From MaRDI portal
Cited in
(20)- Formalization of the resolution calculus for first-order logic
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Abstract Completeness
- Completeness theorem
- FOL Fitting
- Abstract Soundness
- Incompleteness Theorems
- Logtk
- Paraconsistency
- Incredible Proof Machine
- Propositional Resolution
- Nested Multisets
- Verified Prover
- FOL_Harrison
- Ordered_Resolution_Prover
- Saturation_Framework
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Robinson arithmetic
- Epistemic Logic
This page was built for software: Superposition Calculus