Verified Given Clause Procedures

DOI10.1007/978-3-031-38499-8_4MaRDI QIDQ6492729zbMATH OpenFDO

Authors Jasmin Christian Blanchette, Qi Qiu, Sophie Tourret

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_4

Mathematics Subject Classification ID

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

Cites work

• A comprehensive framework for saturation theorem proving
• A comprehensive framework for saturation theorem proving
• A Machine-Oriented Logic Based on the Resolution Principle
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• scientific article; zbMATH DE number 7204438 (Why is no real title available?)
• Implementing Superposition in iProver (System Description)
• Isabelle/HOL. A proof assistant for higher-order logic
• Making higher-order superposition work
• Resolution theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Superposition for full higher-order logic

Cited in

(1)

• Duper: a proof-producing superposition theorem prover for dependent type theory

This page was built for publication: Verified Given Clause Procedures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6492729)