Baaz, Matthias; Moser, Georg Herbrand’s theorem and term induction. (English) Zbl 1093.03032 Arch. Math. Logic 45, No. 4, 447-503 (2006). Reviewer: Branislav Boričić (Beograd) MSC: 03F07 03F20 03B10 03B35 PDFBibTeX XMLCite \textit{M. Baaz} and \textit{G. Moser}, Arch. Math. Logic 45, No. 4, 447--503 (2006; Zbl 1093.03032) Full Text: DOI
Bolc, Leonard; Borowik, Piotr Many-valued logics 2. Automated reasoning and practical applications. (English) Zbl 1034.03001 Berlin: Springer (ISBN 3-540-64507-1/hbk). xi, 303 p. (2003). Reviewer: Siegfried J. Gottwald (Leipzig) MSC: 03-02 03B50 03F05 03B35 68Q60 68T15 94D05 94C10 03E72 68T30 PDFBibTeX XMLCite \textit{L. Bolc} and \textit{P. Borowik}, Many-valued logics 2. Automated reasoning and practical applications. Berlin: Springer (2003; Zbl 1034.03001)
Kunen, Kenneth Nonconstructive computational mathematics. (English) Zbl 0922.03076 J. Autom. Reasoning 21, No. 1, 69-97 (1998). Reviewer: M.Yasuhara (Princeton) MSC: 03F30 03B35 03D20 68T15 PDFBibTeX XMLCite \textit{K. Kunen}, J. Autom. Reasoning 21, No. 1, 69--97 (1998; Zbl 0922.03076) Full Text: DOI
Kunen, Kenneth A Ramsey theorem in Boyer-Moore logic. (English) Zbl 0836.03031 J. Autom. Reasoning 15, No. 2, 217-235 (1995). MSC: 03F30 03-04 68T15 PDFBibTeX XMLCite \textit{K. Kunen}, J. Autom. Reasoning 15, No. 2, 217--235 (1995; Zbl 0836.03031) Full Text: DOI
Boyer, R. S.; Moore, J. S. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. (English) Zbl 0678.68091 Logic and the acquisition of knowledge, Mach. Intell. 11, 83-124 (1988). MSC: 68T15 03F30 PDFBibTeX XML
Coquand, Thierry; Huet, Gérard A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction. (English) Zbl 0591.68036 J. Symb. Comput. 1, 323-328 (1985). MSC: 68Q65 68Q60 03Fxx 03B35 03B15 03B40 03F55 68T15 00A15 PDFBibTeX XMLCite \textit{T. Coquand} and \textit{G. Huet}, J. Symb. Comput. 1, 323--328 (1985; Zbl 0591.68036) Full Text: DOI