Formalizing Bachmair and Ganzinger's ordered resolution prover

DOI10.1007/978-3-319-94205-6_7zbMath1468.68306OpenAlexW2787490662MaRDI QIDQ5916290

Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann, Anders Schlichtkrull

Publication date: 18 October 2018

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/1871.1/09bae484-e3f3-4ea4-a2a6-77e59679a235

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (9)

Formalization of the resolution calculus for first-order logic ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Superposition with lambdas ⋮ A comprehensive framework for saturation theorem proving ⋮ Distilling the requirements of Gödel's incompleteness theorems with a proof assistant ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ A formally verified abstract account of Gödel's incompleteness theorems ⋮ Formalization of the Resolution Calculus for First-Order Logic ⋮ A comprehensive framework for saturation theorem proving

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• HOL
• Isabelle/jEdit
• CeTA
• Locales
• Superposition Calculus
• Logtk
• AVATAR

This page was built for publication: Formalizing Bachmair and Ganzinger's ordered resolution prover