Pages that link to "Item:Q1006729"
From MaRDI portal
The following pages link to Efficiently checking propositional refutations in HOL theorem provers (Q1006729):
Displaying 14 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Resolution proof transformation for compression and interpolation (Q479815) (← links)
- Data compression for proof replay (Q1040776) (← links)
- Quantum adiabatic machine learning (Q2393692) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- Functional Encryption for Inner Product with Full Function Privacy (Q2798775) (← links)
- Validating QBF Validity in HOL4 (Q3088005) (← links)
- Proving Valid Quantified Boolean Formulas in HOL Light (Q3088006) (← links)
- LCF-Style Bit-Blasting in HOL4 (Q3088019) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL (Q3100212) (← links)
- LCF-Style Propositional Simplification with BDDs and SAT Solvers (Q3543649) (← links)
- Imperative Functional Programming with Isabelle/HOL (Q3543655) (← links)
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme (Q3655207) (← links)
