Validating QBF Validity in HOL4 (Q3088005): Difference between revisions

@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-22863-6_14
+Normal rank
@@ Property / OpenAlex ID @@
+W4232871528
@@ Property / OpenAlex ID: W4232871528 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Q3620436
@@ Property / cites work: Q3620436 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4131648
@@ Property / cites work: Q4131648 / rank @@
+Normal rank
@@ Property / cites work @@
+Evaluating and certifying QBFs: A comparison of state-of-the-art tools
+Normal rank
@@ Property / cites work @@
+A First Step Towards a Unified Proof Checker for QBF
+Normal rank
@@ Property / cites work @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+A Short Presentation of Coq
@@ Property / cites work: A Short Presentation of Coq / rank @@
+Normal rank
@@ Property / cites work @@
+The Isabelle Framework
@@ Property / cites work: The Isabelle Framework / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of PVS
@@ Property / cites work: A Brief Overview of PVS / rank @@
+Normal rank
@@ Property / cites work @@
+Efficiently checking propositional refutations in HOL theorem provers
+Normal rank
@@ Property / cites work @@
+Fast LCF-Style Proof Reconstruction for Z3
@@ Property / cites work: Fast LCF-Style Proof Reconstruction for Z3 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809048
@@ Property / cites work: Q4809048 / rank @@
+Normal rank
@@ Property / cites work @@
+Translating higher-order clauses to first-order clauses
+Normal rank
@@ Property / cites work @@
+Q4412858
@@ Property / cites work: Q4412858 / rank @@
+Normal rank
@@ Property / cites work @@
+Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas
+Normal rank
@@ Property / cites work @@
+Q3429159
@@ Property / cites work: Q3429159 / rank @@
+Normal rank
@@ Property / cites work @@
+Validating QBF Invalidity in HOL4
@@ Property / cites work: Validating QBF Invalidity in HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+Resolution for quantified Boolean formulas
@@ Property / cites work: Resolution for quantified Boolean formulas / rank @@
+Normal rank
@@ Property / cites work @@
+Combining Coq and Gappa for Certifying Floating-Point Programs
+Normal rank
@@ Property / cites work @@
+MetiTarski: An automatic theorem prover for real-valued special functions
+Normal rank
@@ Property / cites work @@
+A formulation of the simple theory of types
@@ Property / cites work: A formulation of the simple theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754029
@@ Property / cites work: Q2754029 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic versus Approximation
@@ Property / cites work: Logic versus Approximation / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
+Normal rank