Efficiently checking propositional refutations in HOL theorem provers

DOI10.1016/j.jal.2007.07.003zbMath1171.68041OpenAlexW2168950896MaRDI QIDQ1006729

Hasan Amjad, Tjark Weber

Publication date: 25 March 2009

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2007.07.003

zbMATH Keywords

interactive theorem provingLCF-style proof checkingpropositional resolution

Mathematics Subject Classification ID

Related Items

The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Quantum adiabatic machine learning ⋮ SMT proof checking using a logical framework ⋮ LCF-Style Propositional Simplification with BDDs and SAT Solvers ⋮ Imperative Functional Programming with Isabelle/HOL ⋮ Resolution proof transformation for compression and interpolation ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ Validating QBF Validity in HOL4 ⋮ Proving Valid Quantified Boolean Formulas in HOL Light ⋮ LCF-Style Bit-Blasting in HOL4 ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme ⋮ Data compression for proof replay

Uses Software

• ACL2
• Isabelle
• MiniSat
• ML
• Isabelle/HOL
• SATLIB
• PVS
• zChaff
• HOL Light
• Chaff
• CVC Lite
• LCF
• Gandalf
• TRAMP

Cites Work

• Applying SAT solving in classification of finite algebras
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
• Compressing Propositional Refutations
• Automated Reasoning
• Computer Aided Verification
• Theory and Applications of Satisfiability Testing
• Theorem Proving in Higher Order Logics
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Tools and Algorithms for the Construction and Analysis of Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Efficiently checking propositional refutations in HOL theorem provers