@article{Weber2009,
abstract = {This paper describes the integration of zChaff and MiniSat, currently two leading SAT solvers, with Higher Order Logic (HOL) theorem provers. Both SAT solvers generate resolution-style proofs for (instances of) propositional tautologies. These proofs are verified by the theorem provers. The presented approach significantly improves the provers' performance on propositional problems, and exhibits counterexamples for unprovable conjectures. It is also shown that LCF-style theorem provers can serve as viable proof checkers even for large SAT problems. An efficient representation of the propositional problem in the theorem prover turns out to be crucial; several possible solutions are discussed. ?? 2007 Elsevier Inc. All rights reserved.},
author = {Weber, Tjark and Amjad, Hasan},
doi = {10.1016/j.jal.2007.07.003},
file = {:Users/jonaprieto/Mendeley/Weber, Amjad - 2009 - Efficiently checking propositional refutations in HOL theorem provers.pdf:pdf},
issn = {15708683},
journal = {Journal of Applied Logic},
keywords = {Interactive theorem proving,LCF-style proof checking,Propositional resolution},
number = {1},
pages = {26--40},
title = {{Efficiently checking propositional refutations in HOL theorem provers}},
volume = {7},
year = {2009}
}

{"_id":"g89pQpori5ikB6gfS","bibbaseid":"weber-amjad-efficientlycheckingpropositionalrefutationsinholtheoremprovers-2009","downloads":0,"creationDate":"2017-09-01T03:35:40.585Z","title":"Efficiently checking propositional refutations in HOL theorem provers","author_short":["Weber, T.","Amjad, H."],"year":2009,"bibtype":"article","biburl":"https://raw.githubusercontent.com/jonaprieto/athena/master/paper/ref.bib","bibdata":{"bibtype":"article","type":"article","abstract":"This paper describes the integration of zChaff and MiniSat, currently two leading SAT solvers, with Higher Order Logic (HOL) theorem provers. Both SAT solvers generate resolution-style proofs for (instances of) propositional tautologies. These proofs are verified by the theorem provers. The presented approach significantly improves the provers' performance on propositional problems, and exhibits counterexamples for unprovable conjectures. It is also shown that LCF-style theorem provers can serve as viable proof checkers even for large SAT problems. An efficient representation of the propositional problem in the theorem prover turns out to be crucial; several possible solutions are discussed. ?? 2007 Elsevier Inc. All rights reserved.","author":[{"propositions":[],"lastnames":["Weber"],"firstnames":["Tjark"],"suffixes":[]},{"propositions":[],"lastnames":["Amjad"],"firstnames":["Hasan"],"suffixes":[]}],"doi":"10.1016/j.jal.2007.07.003","file":":Users/jonaprieto/Mendeley/Weber, Amjad - 2009 - Efficiently checking propositional refutations in HOL theorem provers.pdf:pdf","issn":"15708683","journal":"Journal of Applied Logic","keywords":"Interactive theorem proving,LCF-style proof checking,Propositional resolution","number":"1","pages":"26--40","title":"Efficiently checking propositional refutations in HOL theorem provers","volume":"7","year":"2009","bibtex":"@article{Weber2009,\nabstract = {This paper describes the integration of zChaff and MiniSat, currently two leading SAT solvers, with Higher Order Logic (HOL) theorem provers. Both SAT solvers generate resolution-style proofs for (instances of) propositional tautologies. These proofs are verified by the theorem provers. The presented approach significantly improves the provers' performance on propositional problems, and exhibits counterexamples for unprovable conjectures. It is also shown that LCF-style theorem provers can serve as viable proof checkers even for large SAT problems. An efficient representation of the propositional problem in the theorem prover turns out to be crucial; several possible solutions are discussed. ?? 2007 Elsevier Inc. All rights reserved.},\nauthor = {Weber, Tjark and Amjad, Hasan},\ndoi = {10.1016/j.jal.2007.07.003},\nfile = {:Users/jonaprieto/Mendeley/Weber, Amjad - 2009 - Efficiently checking propositional refutations in HOL theorem provers.pdf:pdf},\nissn = {15708683},\njournal = {Journal of Applied Logic},\nkeywords = {Interactive theorem proving,LCF-style proof checking,Propositional resolution},\nnumber = {1},\npages = {26--40},\ntitle = {{Efficiently checking propositional refutations in HOL theorem provers}},\nvolume = {7},\nyear = {2009}\n}\n","author_short":["Weber, T.","Amjad, H."],"key":"Weber2009","id":"Weber2009","bibbaseid":"weber-amjad-efficientlycheckingpropositionalrefutationsinholtheoremprovers-2009","role":"author","urls":{},"keyword":["Interactive theorem proving","LCF-style proof checking","Propositional resolution"],"downloads":0},"search_terms":["efficiently","checking","propositional","refutations","hol","theorem","provers","weber","amjad"],"keywords":["interactive theorem proving","lcf-style proof checking","propositional resolution"],"authorIDs":[],"dataSources":["8jafqMAWgB7XP4FTZ"]}