Brüning, Stefan Exploiting equivalences in connection calculi. (English) Zbl 0856.03009 J. IGPL 3, No. 6, 857-886 (1995). Reviewer: A.Leitsch (Wien) MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{S. Brüning}, J. IGPL 3, No. 6, 857--886 (1995; Zbl 0856.03009)
Baaz, Matthias; Leitsch, Alexander On Skolemization and proof complexity. (English) Zbl 0815.03003 Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 20, No. 4, 353-379 (1994). Reviewer: A.Leitsch (Wien) MSC: 03B35 68T15 03F20 PDFBibTeX XMLCite \textit{M. Baaz} and \textit{A. Leitsch}, Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 20, No. 4, 353--379 (1994; Zbl 0815.03003)
Wu, Wen-tsün Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang. (English) Zbl 0831.03003 Texts and Monographs in Symbolic Computation. Berlin: Springer-Verlag. 300 p. DM 98.00 /sc (1994). Reviewer: A.Leitsch (Wien) MSC: 03B35 03-02 68T15 68W30 68-02 68U05 14Qxx PDFBibTeX XMLCite \textit{W.-t. Wu}, Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang. Berlin: Springer (1994; Zbl 0831.03003)
Doets, Kees Levationis laus. (English) Zbl 0807.03004 J. Log. Comput. 3, No. 5, 487-516 (1993). Reviewer: A.Leitsch (Wien) MSC: 03B35 68N17 PDFBibTeX XMLCite \textit{K. Doets}, J. Log. Comput. 3, No. 5, 487--516 (1993; Zbl 0807.03004) Full Text: DOI
Bundy, Alan; Stevens, Andrew; van Harmelen, Frank; Ireland, Andrew; Smaill, Alan Rippling: A heuristic for guiding inductive proofs. (English) Zbl 0789.68121 Artif. Intell. 62, No. 2, 185-253 (1993). Reviewer: A.Leitsch (Wien) MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{A. Bundy} et al., Artif. Intell. 62, No. 2, 185--253 (1993; Zbl 0789.68121) Full Text: DOI
Giordano, Laura; Martelli, Alberto; Rossi, Gianfranco Extending Horn clause logic with implication goals. (English) Zbl 0754.68109 Theor. Comput. Sci. 95, No. 1, 43-74 (1992). Reviewer: A.Leitsch (Wien) MSC: 68T27 68T99 PDFBibTeX XMLCite \textit{L. Giordano} et al., Theor. Comput. Sci. 95, No. 1, 43--74 (1992; Zbl 0754.68109) Full Text: DOI
Kröger, Fred Einführung in die Informatik. Algorithmenentwicklung. (Introduction into computer science. Development of algorithms.). (German) Zbl 0726.68003 Springer-Lehrbuch. Berlin etc.: Springer-Verlag. X, 318 p. DM 46.00 (1991). Reviewer: A.Leitsch (Wien) MSC: 68-01 68Q60 68N01 68Q99 PDFBibTeX XMLCite \textit{F. Kröger}, Einführung in die Informatik. Algorithmenentwicklung. (Introduction into computer science. Development of algorithms.). Berlin etc.: Springer-Verlag (1991; Zbl 0726.68003)
Allen, Bill Arithmetizing uniform \(NC\). (English) Zbl 0741.03019 Ann. Pure Appl. Logic 53, No. 1, 1-50 (1991). Reviewer: A.Leitsch (Wien) MSC: 03D15 03F30 68Q15 PDFBibTeX XMLCite \textit{B. Allen}, Ann. Pure Appl. Logic 53, No. 1, 1--50 (1991; Zbl 0741.03019) Full Text: DOI
Sato, Taisuke Completed logic programs and their consistency. (English) Zbl 0715.68011 J. Logic Program. 9, No. 1, 33-44 (1990). Reviewer: A.Leitsch MSC: 68N17 68T15 68N01 PDFBibTeX XMLCite \textit{T. Sato}, J. Log. Program. 9, No. 1, 33--44 (1990; Zbl 0715.68011) Full Text: DOI
Wolfram, D. A. Intractable unifiability problems and backtracking. (English) Zbl 0686.68043 J. Autom. Reasoning 5, No. 1, 37-47 (1989). Reviewer: A.Leitsch MSC: 68Q25 68T15 PDFBibTeX XMLCite \textit{D. A. Wolfram}, J. Autom. Reasoning 5, No. 1, 37--47 (1989; Zbl 0686.68043) Full Text: DOI
Calude, C.; Chitescu, I. Upper limitation of Kolmogorov complexity and universal P. Martin-Löf tests. (English) Zbl 0673.68028 J. Comput. Math. 7, No. 1, 61-70 (1989). Reviewer: A.Leitsch MSC: 68Q25 03D20 03D15 PDFBibTeX XMLCite \textit{C. Calude} and \textit{I. Chitescu}, J. Comput. Math. 7, No. 1, 61--70 (1989; Zbl 0673.68028)
Kleine Büning, Hans; Löwen, Ulrich Optimizing propositional calculus formulas with regard to questions of deducibility. (English) Zbl 0668.03004 Inf. Comput. 80, No. 1, 18-43 (1989). Reviewer: A.Leitsch MSC: 03B35 03F20 68T15 03B25 68Q25 PDFBibTeX XMLCite \textit{H. Kleine Büning} and \textit{U. Löwen}, Inf. Comput. 80, No. 1, 18--43 (1989; Zbl 0668.03004) Full Text: DOI
Leitsch, Alexander On different concepts of resolution. (English) Zbl 0646.03011 Z. Math. Logik Grundlagen Math. 35, No. 1, 71-77 (1989). Reviewer: A.Leitsch MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{A. Leitsch}, Z. Math. Logik Grundlagen Math. 35, No. 1, 71--77 (1989; Zbl 0646.03011) Full Text: DOI
Grabowski, Jan; Jantke, Klaus P.; Thiele, Helmut Grundlagen der Künstlichen Intelligenz. (German) Zbl 0699.68002 Informatik, Kybernetik, Rechentechnik, 31. Berlin, GDR: Akademie-Verlag. 296 p. DM 65.00 (1989). Reviewer: A.Leitsch MSC: 68-01 03B35 68T15 68T99 PDFBibTeX XMLCite \textit{J. Grabowski} et al., Grundlagen der Künstlichen Intelligenz. Berlin, GDR: Akademie-Verlag (1989; Zbl 0699.68002)
Wu, Maokang Input semi-lock refutation on Horn set with equality. (English) Zbl 0683.03006 Kexue Tongbao, Sci. Bull. 33, No. 15, 1233-1234 (1988). Reviewer: A.Leitsch MSC: 03B35 PDFBibTeX XMLCite \textit{M. Wu}, Kexue Tongbao, Sci. Bull. 33, No. 15, 1233--1234 (1988; Zbl 0683.03006)
Auffray, Yves Linear strategy for propositional modal resolution. (English) Zbl 0662.03006 Inf. Process. Lett. 28, No. 2, 87-92 (1988). Reviewer: A.Leitsch MSC: 03B35 03B45 PDFBibTeX XMLCite \textit{Y. Auffray}, Inf. Process. Lett. 28, No. 2, 87--92 (1988; Zbl 0662.03006) Full Text: DOI
McCarty, L. Thorne Clausal intuitionistic logic. II. Tableau proof procedures. (English) Zbl 0661.03004 J. Logic Program. 5, No. 2, 93-132 (1988). Reviewer: A.Leitsch MSC: 03B20 68T15 03B35 03F07 PDFBibTeX XMLCite \textit{L. T. McCarty}, J. Log. Program. 5, No. 2, 93--132 (1988; Zbl 0661.03004) Full Text: DOI
Shankar, N. A mechanical proof of the Church-Rosser theorem. (English) Zbl 0654.68103 J. Assoc. Comput. Mach. 35, No. 3, 475-522 (1988). Reviewer: A.Leitsch MSC: 68T15 03B35 03B40 PDFBibTeX XMLCite \textit{N. Shankar}, J. Assoc. Comput. Mach. 35, No. 3, 475--522 (1988; Zbl 0654.68103) Full Text: DOI
Kounalis, Emmanuel; Rusinowitch, Michael On word problems in Horn theories. (English) Zbl 0653.03030 Automated deduction, Proc. 9th Int. Conf., Argonne/Ill. 1988, Lect. Notes Comput. Sci. 310, 527-537 (1988). Reviewer: A.Leitsch MSC: 03D40 03B35 PDFBibTeX XML
McCarty, L. Thorne Clausal intuitionistic logic. I: Fixed-point semantics. (English) Zbl 0645.03006 J. Logic Program. 5, No. 1, 1-31 (1988). Reviewer: A.Leitsch MSC: 03B20 68T15 03B35 PDFBibTeX XMLCite \textit{L. T. McCarty}, J. Log. Program. 5, No. 1, 1--31 (1988; Zbl 0645.03006) Full Text: DOI
Haeusler, Edward Hermann Automatic theorem proving: An attempt to improve readability of proofs generated by resolution. (English) Zbl 0641.03011 Methods and applications of mathematical logic, Proc. 7th Lat. Am. Symp. Math. Logic, Campinas/Braz. 1985, Contemp. Math. 69, 179-188 (1988). Reviewer: A.Leitsch MSC: 03B35 68T15 PDFBibTeX XML
Calude, Cristian Theories of computational complexity. (English) Zbl 0633.03034 Annals of Discrete Mathematics, 35. Amsterdam etc.: North-Holland. XII, 487 p. (1988). Reviewer: A.Leitsch MSC: 03D15 68Q25 03D60 03D20 03-02 68-02 PDFBibTeX XMLCite \textit{C. Calude}, Theories of computational complexity. Amsterdam etc.: North-Holland (1988; Zbl 0633.03034)
Cohn, Anthony G. A more expressive formulation of many sorted logic. (English) Zbl 0642.68166 J. Autom. Reasoning 3, 113-200 (1987). Reviewer: A.Leitsch MSC: 68T15 03B10 PDFBibTeX XMLCite \textit{A. G. Cohn}, J. Autom. Reasoning 3, 113--200 (1987; Zbl 0642.68166) Full Text: DOI
Chou, Shang-Ching A method for the mechanical derivation of formulas in elementary geometry. (English) Zbl 0638.68109 J. Autom. Reasoning 3, 291-299 (1987). Reviewer: A.Leitsch MSC: 68T15 68W30 03B35 PDFBibTeX XMLCite \textit{S.-C. Chou}, J. Autom. Reasoning 3, 291--299 (1987; Zbl 0638.68109) Full Text: DOI
Hsiang, Jieh Rewrite method for theorem proving in first order theory with equality. (English) Zbl 0637.68104 J. Symb. Comput. 3, 133-151 (1987). Reviewer: A.Leitsch MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{J. Hsiang}, J. Symb. Comput. 3, 133--151 (1987; Zbl 0637.68104) Full Text: DOI
Haken, Armin The intractability of resolution. (English) Zbl 0586.03010 Theor. Comput. Sci. 39, 297-308 (1985). Reviewer: A.Leitsch MSC: 03B35 03D15 03F20 03B05 68Q25 PDFBibTeX XMLCite \textit{A. Haken}, Theor. Comput. Sci. 39, 297--308 (1985; Zbl 0586.03010) Full Text: DOI
Hong, Jiawei The complexity of formal proving. (English) Zbl 0577.03027 Sci. Sin., Ser. A 27, 1046-1054 (1984). Reviewer: A.Leitsch MSC: 03F20 03B35 03D15 03D10 PDFBibTeX XMLCite \textit{J. Hong}, Sci. Sin., Ser. A 27, 1046--1054 (1984; Zbl 0577.03027)
Mart’yanov, V. I. Invariant transformations of formulas. (English. Russian original) Zbl 0577.03002 Math. Notes 36, 782-788 (1984); translation from Mat. Zametki 36, No. 4, 571-582 (1984). Reviewer: A.Leitsch MSC: 03B35 03C99 03B10 PDFBibTeX XMLCite \textit{V. I. Mart'yanov}, Math. Notes 36, 782--788 (1984; Zbl 0577.03002); translation from Mat. Zametki 36, No. 4, 571--582 (1984) Full Text: DOI
Lenat, Douglas B. Automated theory formation in mathematics. (English) Zbl 0563.68073 Automated theorem proving, Proc. Spec. Sess., 89th Meet. Am. Math. Soc., Denver/Colo. 1983, Contemp. Math. 29, 287-314 (1984). Reviewer: A.Leitsch MSC: 68T99 68T15 PDFBibTeX XML
Yamasaki, Susumu; Yoshida, Mikio; Doshita, Shuji; Hirata, Mikito A new combination of input and unit deductions for Horn sentences. (English) Zbl 0563.68072 Inf. Process. Lett. 18, 209-213 (1984). Reviewer: A.Leitsch MSC: 68T15 68N01 03B35 PDFBibTeX XMLCite \textit{S. Yamasaki} et al., Inf. Process. Lett. 18, 209--213 (1984; Zbl 0563.68072) Full Text: DOI
Wos, L.; Winker, S.; Smith, B. A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains. (English) Zbl 0553.68051 Artif. Intell. 22, 303-356 (1984). Reviewer: A.Leitsch MSC: 68T15 03-04 03B60 PDFBibTeX XMLCite \textit{L. Wos} et al., Artif. Intell. 22, 303--356 (1984; Zbl 0553.68051) Full Text: DOI
Loveland, Donald W. Automated theorem-proving: A quarter-century review. (English) Zbl 0553.68050 Automated theorem proving, Proc. Spec. Sess., 89th Meet. Am. Math. Soc., Denver/Colo. 1983, Contemp. Math. 29, 1-45 (1984). Reviewer: A.Leitsch MSC: 68T15 68-02 68-03 01A60 01A65 PDFBibTeX XML
Furst, Merrick; Saxe, James B.; Sipser, Michael Parity, circuits, and the polynomial-time hierarchy. (English) Zbl 0534.94008 Math. Syst. Theory 17, 13-27 (1984). Reviewer: A.Leitsch MSC: 94C10 68Q25 03D15 PDFBibTeX XMLCite \textit{M. Furst} et al., Math. Syst. Theory 17, 13--27 (1984; Zbl 0534.94008) Full Text: DOI
Tovey, Craig A. A simplified NP-complete satisfiability problem. (English) Zbl 0534.68028 Discrete Appl. Math. 8, 85-89 (1984). Reviewer: A.Leitsch MSC: 68Q25 68T15 03-04 PDFBibTeX XMLCite \textit{C. A. Tovey}, Discrete Appl. Math. 8, 85--89 (1984; Zbl 0534.68028) Full Text: DOI
Arnon, Dennis S.; Smith, Scott F. Towards mechanical solution of the Kahan ellipse problem. I. (English) Zbl 0553.68031 Computer algebra, EUROCAL ’83, Proc. Conf., London 1983, Lect. Notes Comput. Sci. 162, 36-44 (1983). Reviewer: A.Leitsch MSC: 68W30 68T15 03C10 03B35 12L12 12D15 PDFBibTeX XML
Makarov, V. P. On theory of abstract algorithms. (English. Russian original) Zbl 0539.68020 Autom. Doc. Math. Linguist. 16, No. 5, 61-75 (1982); translation from Nauchno-Tekh. Inf., Ser. 2 1982, No. 9, 35-40 (1982). Reviewer: A.Leitsch MSC: 68W99 68Q60 68Q55 PDFBibTeX XMLCite \textit{V. P. Makarov}, Autom. Doc. Math. Linguist. 16, No. 5, 61--75 (1982; Zbl 0539.68020); translation from Nauchno-Tekh. Inf., Ser. 2 1982, No. 9, 35--40 (1982)