Verified Given Clause Procedures
From MaRDI portal
Publication:6492729
DOI10.1007/978-3-031-38499-8_4MaRDI QIDQ6492729
Qi Qiu, Sophie Tourret, Jasmin Christian Blanchette
Publication date: 26 April 2024
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Unnamed Item
- Unnamed Item
- Isabelle/HOL. A proof assistant for higher-order logic
- Superposition for full higher-order logic
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Implementing Superposition in iProver (System Description)
- A Machine-Oriented Logic Based on the Resolution Principle
- Making higher-order superposition work
- A comprehensive framework for saturation theorem proving
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A comprehensive framework for saturation theorem proving
This page was built for publication: Verified Given Clause Procedures
