Wu, Chih-Hung; Lee, Shie-Jue Parallelization of a hyper-linking-based theorem prover. (English) Zbl 0958.03013 J. Autom. Reasoning 26, No. 1, 67-106 (2001). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{C.-H. Wu} and \textit{S.-J. Lee}, J. Autom. Reasoning 26, No. 1, 67--106 (2001; Zbl 0958.03013) Full Text: DOI
Nipkow, Tobias More Church-Rosser proofs (in Isabelle/HOL). (English) Zbl 0958.03011 J. Autom. Reasoning 26, No. 1, 51-66 (2001). MSC: 03B35 03B40 68T15 PDFBibTeX XMLCite \textit{T. Nipkow}, J. Autom. Reasoning 26, No. 1, 51--66 (2001; Zbl 0958.03011) Full Text: DOI
Giesl, Jürgen Induction proofs with partial functions. (English) Zbl 0971.03016 J. Autom. Reasoning 26, No. 1, 1-49 (2001). Reviewer: N.Ţăndăreanu (Craiova) MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{J. Giesl}, J. Autom. Reasoning 26, No. 1, 1--49 (2001; Zbl 0971.03016) Full Text: DOI