Encoding First Order Proofs in SMT

DOI10.1016/j.entcs.2008.04.081zbMath1277.03006OpenAlexW1975097530WikidataQ118190444 ScholiaQ118190444MaRDI QIDQ2864408

Ralph Eric McGgregor, Jeremy Bongio, Hai Lin, Cyrus Katrak, Christopher Lynch

Publication date: 6 December 2013

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.04.081

zbMATH Keywords

first-order logictableauSMTYices

Mathematics Subject Classification ID

Related Items (1)

Theorem proving as constraint solving with coherent logic

Uses Software

• MiniSat
• TPTP
• Yices

Cites Work

• The TPTP problem library. CNF release v1. 2. 1
• Solving SAT and SAT Modulo Theories
• Protocol Verification Via Rigid/Flexible Resolution
• Encoding First Order Proofs in SAT
• Theorem Proving via General Matings
• A machine program for theorem-proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Encoding First Order Proofs in SMT