Efficiently checking propositional refutations in HOL theorem provers (Q1006729): Difference between revisions

@@ Property / DOI @@
-.1016/j.jal.2007.07.003
@@ Property / DOI: 10.1016/j.jal.2007.07.003 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+MiniSat
@@ Property / describes a project that uses: MiniSat / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CVC Lite
@@ Property / describes a project that uses: CVC Lite / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Chaff
@@ Property / describes a project that uses: Chaff / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TRAMP
@@ Property / describes a project that uses: TRAMP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+zChaff
@@ Property / describes a project that uses: zChaff / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LCF
@@ Property / describes a project that uses: LCF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SATLIB
@@ Property / describes a project that uses: SATLIB / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Gandalf
@@ Property / describes a project that uses: Gandalf / 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.1016/j.jal.2007.07.003
+Normal rank
@@ Property / OpenAlex ID @@
+W2168950896
@@ Property / OpenAlex ID: W2168950896 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809056
@@ Property / cites work: Q4809056 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Compressing Propositional Refutations
@@ Property / cites work: Compressing Propositional Refutations / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Geometric Resolution: A Proof Procedure Based on Finite Model Search
+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 @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2749862
@@ Property / cites work: Q2749862 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809048
@@ Property / cites work: Q4809048 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2848688
@@ Property / cites work: Q2848688 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723444
@@ Property / cites work: Q2723444 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning
@@ Property / cites work: Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Applying SAT solving in classification of finite algebras
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q4249904
@@ Property / cites work: Q4249904 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
+Normal rank
@@ Property / cites work @@
+Q4790648
@@ Property / cites work: Q4790648 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4427902
@@ Property / cites work: Q4427902 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5604434
@@ Property / cites work: Q5604434 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2848690
@@ Property / cites work: Q2848690 / 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 / DOI @@
+.1016/J.JAL.2007.07.003
@@ Property / DOI: 10.1016/J.JAL.2007.07.003 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:1006729