Baumgartner, Peter; Fuchs, Alexander; de Nivelle, Hans; Tinelli, Cesare Computing finite models by reduction to function-free clause logic. (English) Zbl 1171.68040 J. Appl. Log. 7, No. 1, 58-74 (2009). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{P. Baumgartner} et al., J. Appl. Log. 7, No. 1, 58--74 (2009; Zbl 1171.68040) Full Text: DOI
Weber, Tjark; Amjad, Hasan Efficiently checking propositional refutations in HOL theorem provers. (English) Zbl 1171.68041 J. Appl. Log. 7, No. 1, 26-40 (2009). MSC: 68T15 PDFBibTeX XMLCite \textit{T. Weber} and \textit{H. Amjad}, J. Appl. Log. 7, No. 1, 26--40 (2009; Zbl 1171.68041) Full Text: DOI
Kaufmann, Matt; Moore, J Strother; Ray, Sandip; Reeber, Erik Integrating external deduction tools with ACL2. (English) Zbl 1183.68558 J. Appl. Log. 7, No. 1, 3-25 (2009). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{M. Kaufmann} et al., J. Appl. Log. 7, No. 1, 3--25 (2009; Zbl 1183.68558) Full Text: DOI