Encoding First Order Proofs in SAT

DOI10.1007/978-3-540-73595-3_35MaRDI QIDQ3608794zbMATH OpenOpenAlexFDO

Authors Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor

Publication date 6 March 2009

Published in Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73595-3_35

Mathematics Subject Classification ID

Recommendations

• Encoding first order proofs in SMT
• scientific article; zbMATH DE number 1903356
• Reducing higher-order theorem proving to a sequence of SAT problems
• Efficient encodings of first-order Horn formulas in equational logic
• First-order modal tableaux

Cited in

(12)

• Theorem proving as constraint solving with coherent logic
• Eliminating models during model elimination
• SMELS: satisfiability modulo equality with lazy superposition
• Encoding first order proofs in SMT
• Protocol Verification Via Rigid/Flexible Resolution
• Combining instance generation and resolution
• scientific article; zbMATH DE number 2165692 (Why is no real title available?)
• SAT Encoding of Unification in $\mathcal{EL}$
• Constraint learning for non-confluent proof search
• Finding connections via satisfiability solving
• Theorem proving as constraint solving for coherent logic with function symbols
• Automated completion of statements and proofs in synthetic geometry: an approach based on constraint solving

Describes a project that uses

Uses Software

• VAMPIRE

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

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