Understanding Resolution Proofs through Herbrand’s Theorem

DOI10.1007/978-3-642-40537-2_15zbMath1401.03038OpenAlexW104201083MaRDI QIDQ2851942

Tomer Libal, Stefan Hetzl, Mikheil Rukhaia, Martin Riener

Publication date: 4 October 2013

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-40537-2_15

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Related Items (4)

Extraction of expansion trees ⋮ Scalable fine-grained proofs for formula processing ⋮ System Description: GAPT 2.0 ⋮ Complexity of translations from resolution to sequent calculus

Uses Software

• TPTP
• Prover9
• Mace4
• CERES
• Ivy
• TRAMP
• GAPT
• ProofTool

This page was built for publication: Understanding Resolution Proofs through Herbrand’s Theorem