Beeson, Michael; Wos, Larry Finding proofs in Tarskian geometry. (English) Zbl 1414.68100 J. Autom. Reasoning 58, No. 1, 181-207 (2017). MSC: 68T15 51K05 51M05 PDFBibTeX XMLCite \textit{M. Beeson} and \textit{L. Wos}, J. Autom. Reasoning 58, No. 1, 181--207 (2017; Zbl 1414.68100) Full Text: DOI arXiv
Beeson, Michael; Wos, Larry OTTER proofs in Tarskian geometry. (English) Zbl 1414.68099 Demri, Stéphane (ed.) et al., Automated reasoning. 7th international joint conference, IJCAR 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 19–22, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8562, 495-510 (2014). MSC: 68T15 51K05 51M05 PDFBibTeX XMLCite \textit{M. Beeson} and \textit{L. Wos}, Lect. Notes Comput. Sci. 8562, 495--510 (2014; Zbl 1414.68099) Full Text: DOI
Wos, Larry The legacy of a great researcher. (English) Zbl 1383.68004 Bonacina, Maria Paola (ed.) et al., Automated reasoning and mathematics. Essays in memory of William W. McCune. Berlin: Springer (ISBN 978-3-642-36674-1/pbk). Lecture Notes in Computer Science 7788. Lecture Notes in Artificial Intelligence, 1-14 (2013). MSC: 68-03 01A70 68T15 PDFBibTeX XMLCite \textit{L. Wos}, Lect. Notes Comput. Sci. 7788, 1--14 (2013; Zbl 1383.68004) Full Text: DOI
Wos, Larry The flowering of automated reasoning. (English) Zbl 1098.68700 Hutter, Dieter (ed.) et al., Mechanizing mathematical reasoning. Essays in honor of Jörg H. Siekmann on the occasion of his 60th birthday. Berlin: Springer (ISBN 3-540-25051-4/pbk). Lecture Notes in Computer Science 2605. Lecture Notes in Artificial Intelligence, 204-227 (2005). MSC: 68T15 03B35 68-02 68-03 PDFBibTeX XMLCite \textit{L. Wos}, Lect. Notes Comput. Sci. 2605, 204--227 (2005; Zbl 1098.68700) Full Text: DOI
Wos, Larry; Ulrich, Dolph; Fitelson, Branden XCB, the last of the shortest single axioms for the classical equivalential calculus. (English) Zbl 1119.03321 Bull. Sect. Log., Univ. Łódź, Dep. Log. 32, No. 3, 131-136 (2003). MSC: 03B20 03B35 68T15 PDFBibTeX XMLCite \textit{L. Wos} et al., Bull. Sect. Log., Univ. Łódź, Dep. Log. 32, No. 3, 131--136 (2003; Zbl 1119.03321)
Wos, Larry The strategy of cramming. (English) Zbl 1023.68092 J. Autom. Reasoning 30, No. 2, 179-204 (2003). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 30, No. 2, 179--204 (2003; Zbl 1023.68092) Full Text: DOI
Wos, Larry; Pieper, Gail W. Automated reasoning and the discovery of missing and elegant proofs. (English) Zbl 1058.68102 Princeton, NJ: Rinton Press (ISBN 1-58949-023-1/hbk). xv, 372 p. (2003). Reviewer: Jana Koehler (Rüschlikon) MSC: 68T15 68-02 03B35 PDFBibTeX XMLCite \textit{L. Wos} and \textit{G. W. Pieper}, Automated reasoning and the discovery of missing and elegant proofs. Princeton, NJ: Rinton Press (2003; Zbl 1058.68102)
Wos, Larry; Fitelson, Branden The automation of sound reasoning and successful proof finding. (English) Zbl 1064.03011 Jacquette, Dale (ed.), A companion to philosophical logic. Malden, MA: Blackwell Publishers (ISBN 0-631-21671-5/hbk). Blackwell Companions Philos. 22, 709-723 (2002). Reviewer: Nail Zamov (Kazan) MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{L. Wos} and \textit{B. Fitelson}, in: A companion to philosophical logic. Malden, MA: Blackwell Publishers. 709--723 (2002; Zbl 1064.03011)
Ernst, Zachary; Fitelson, Branden; Harris, Kenneth; Wos, Larry Shortest axiomatizations of implicational S4 and S5. (English) Zbl 1045.03021 Notre Dame J. Formal Logic 43, No. 3, 169-179 (2002). Reviewer: Manuel Ojeda Aciego (Malaga) MSC: 03B45 68T15 PDFBibTeX XMLCite \textit{Z. Ernst} et al., Notre Dame J. Formal Logic 43, No. 3, 169--179 (2002; Zbl 1045.03021) Full Text: DOI
McCune, William; Veroff, Robert; Fitelson, Branden; Harris, Kenneth; Feist, Andrew; Wos, Larry Short single axioms for Boolean algebra. (English) Zbl 1014.06012 J. Autom. Reasoning 29, No. 1, 1-16 (2002). MSC: 06E05 06-04 68T15 PDFBibTeX XMLCite \textit{W. McCune} et al., J. Autom. Reasoning 29, No. 1, 1--16 (2002; Zbl 1014.06012) Full Text: DOI
Kalman, John Arnold [Wos, Larry] Automated reasoning with OTTER. With a foreword by Larry Wos. With 1 CD-ROM (Windows, Macintosh and UNIX). (English) Zbl 1009.68145 Princeton, NJ: Rinton Press. xv, 536 p. $88.00 (2001). MSC: 68T15 03B35 68-02 68T27 PDFBibTeX XMLCite \textit{J. A. Kalman}, Automated reasoning with OTTER. With a foreword by Larry Wos. With 1 CD-ROM (Windows, Macintosh and UNIX). Princeton, NJ: Rinton Press (2001; Zbl 1009.68145)
Fitelson, Branden; Wos, Larry Finding missing proofs with automated reasoning. (English) Zbl 0997.03011 Stud. Log. 68, No. 3, 329-356 (2001). Reviewer: N.Zamov (Kazan) MSC: 03B35 03-04 68T15 PDFBibTeX XMLCite \textit{B. Fitelson} and \textit{L. Wos}, Stud. Log. 68, No. 3, 329--356 (2001; Zbl 0997.03011) Full Text: DOI
Wos, Larry Conquering the Meredith single axiom. (English) Zbl 1006.03011 J. Autom. Reasoning 27, No. 2, 175-199 (2001). MSC: 03B35 68T15 03B05 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 27, No. 2, 175--199 (2001; Zbl 1006.03011) Full Text: DOI
Fitelson, Branden; Wos, Larry Axiomatic proofs through automated reasoning. (English) Zbl 1045.03014 Bull. Sect. Log., Univ. Łódź, Dep. Log. 29, No. 1-2, 125-136 (2000). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{B. Fitelson} and \textit{L. Wos}, Bull. Sect. Log., Univ. Łódź, Dep. Log. 29, No. 1--2, 125--136 (2000; Zbl 1045.03014)
Wos, Larry Appendix: conjectures concerning proof, design, and verification. (English) Zbl 0974.68537 Aagaard, Mark (ed.) et al., Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14-18, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1869, 526-533 (2000). MSC: 68T27 68T15 68Q60 PDFBibTeX XMLCite \textit{L. Wos}, Lect. Notes Comput. Sci. 1869, 526--533 (2000; Zbl 0974.68537)
Wos, Larry; Fitelson, Branden Automating the search for answers to open questions. (English) Zbl 0974.68538 Aagaard, Mark (ed.) et al., Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14-18, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1869, 519-525 (2000). MSC: 68T27 68T15 68Q60 PDFBibTeX XMLCite \textit{L. Wos} and \textit{B. Fitelson}, Lect. Notes Comput. Sci. 1869, 519--525 (2000; Zbl 0974.68538)
Wos, Larry; Pieper, Gail W. The collected works of Larry Wos. Vol. 1: Exploring the power of automated reasoning. Vol. 2: Applying automated reasoning to puzzles, problems, and open questions. (English) Zbl 0967.68127 Singapore: World Scientific (ISBN 981-02-4001-5/set; 981-02-4996-9/vol1; 981-02-4998-5/vol2; 978-981-281-341-1/ebook/Vol1; 978-981-281-341-1/ebook/Vol2). xvii, 1639 p. (2000). Reviewer: N.Zamov (Kazan’) MSC: 68T01 68T15 68-02 68T20 PDFBibTeX XMLCite \textit{L. Wos} and \textit{G. W. Pieper}, The collected works of Larry Wos. Vol. 1: Exploring the power of automated reasoning. Vol. 2: Applying automated reasoning to puzzles, problems, and open questions. Singapore: World Scientific (2000; Zbl 0967.68127) Full Text: Link
Wos, Larry; Pieper, Gail W. The hot list strategy. (English) Zbl 0926.68132 J. Autom. Reasoning 22, No. 1, 1-44 (1999). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos} and \textit{G. W. Pieper}, J. Autom. Reasoning 22, No. 1, 1--44 (1999; Zbl 0926.68132) Full Text: DOI
Wos, Larry Automating the search for elegant proofs. (English) Zbl 0910.68196 J. Autom. Reasoning 21, No. 2, 135-175 (1998). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 21, No. 2, 135--175 (1998; Zbl 0910.68196) Full Text: DOI
Wos, Larry OTTER and the Moufang identity problem. (English) Zbl 0855.68088 J. Autom. Reasoning 17, No. 2, 215-257 (1996). MSC: 68T15 68T01 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 17, No. 2, 215--257 (1996; Zbl 0855.68088) Full Text: DOI
Wos, Larry The power of combining resonance with heat. (English) Zbl 0877.68104 J. Autom. Reasoning 17, No. 1, 23-81 (1996). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 17, No. 1, 23--81 (1996; Zbl 0877.68104) Full Text: DOI
Wos, Larry Searching for circles of pure proofs. (English) Zbl 0838.68101 J. Autom. Reasoning 15, No. 3, 279-315 (1995). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 15, No. 3, 279--315 (1995; Zbl 0838.68101) Full Text: DOI
Wos, L. The resonance strategy. (English) Zbl 0815.68090 Comput. Math. Appl. 29, No. 2, 133-178 (1995). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{L. Wos}, Comput. Math. Appl. 29, No. 2, 133--178 (1995; Zbl 0815.68090) Full Text: DOI
Wos, Larry The problem of hyperparamodulation and nuclei. (English) Zbl 0805.68104 J. Autom. Reasoning 12, No. 3, 407-409 (1994). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 12, No. 3, 407--409 (1994; Zbl 0805.68104) Full Text: DOI
Wos, Larry The problem of hyperparamodulation. (English) Zbl 0812.68112 J. Autom. Reasoning 12, No. 2, 265-271 (1994). MSC: 68T15 68T20 68T27 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 12, No. 2, 265--271 (1994; Zbl 0812.68112) Full Text: DOI
Wos, Larry Basic research problems: The problem of strategy and hyperresolution. (English) Zbl 0804.68133 J. Autom. Reasoning 12, No. 1, 133-134 (1994). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 12, No. 1, 133--134 (1994; Zbl 0804.68133) Full Text: DOI
Wos, Larry The problem of reasoning by case analysis. (English) Zbl 0802.68134 J. Autom. Reasoning 11, No. 2, 289-291 (1993). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 11, No. 2, 289--291 (1993; Zbl 0802.68134) Full Text: DOI
Wos, Larry The problem of induction. (English) Zbl 0802.68135 J. Autom. Reasoning 11, No. 3, 433-434 (1993). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 11, No. 3, 433--434 (1993; Zbl 0802.68135) Full Text: DOI
Wos, Larry The problem of automated theorem finding. (English) Zbl 0783.68112 J. Autom. Reasoning 10, No. 1, 137-138 (1993). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 10, No. 1, 137--138 (1993; Zbl 0783.68112) Full Text: DOI
Wos, Larry The problem of selecting an approach based on prior success. (English) Zbl 0783.68113 J. Autom. Reasoning 10, No. 2, 283-284 (1993). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 10, No. 2, 283--284 (1993; Zbl 0783.68113) Full Text: DOI
Wos, Larry The problem of reasoning by analogy. (English) Zbl 0783.68114 J. Autom. Reasoning 10, No. 3, 421-422 (1993). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 10, No. 3, 421--422 (1993; Zbl 0783.68114) Full Text: DOI
Wos, Larry The kernel strategy and its use for the study of combinatory logic. (English) Zbl 0802.03010 J. Autom. Reasoning 10, No. 3, 287-343 (1993); erratum ibid. 25, 165 (2000). Reviewer: C.Masalagiu (Iaşi) MSC: 03B40 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 10, No. 3, 287--343 (1993; Zbl 0802.03010) Full Text: DOI
Wos, Larry The problem of naming and function replacement. (English) Zbl 0783.68115 J. Autom. Reasoning 11, No. 1, 147-148 (1993). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 11, No. 1, 147--148 (1993; Zbl 0783.68115) Full Text: DOI
Wos, Larry The problem of reasoning from inequalities. (English) Zbl 0749.68082 J. Autom. Reasoning 8, No. 3, 421-426 (1992). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 8, No. 3, 421--426 (1992; Zbl 0749.68082) Full Text: DOI
Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim Automated reasoning: introduction and applications. Incl. 1 disk. 2nd ed. (English) Zbl 0820.68116 New York, NY: McGraw-Hill,. xvi, 656 p. (1992). MSC: 68T27 68-01 94C10 68T35 68T15 PDFBibTeX XMLCite \textit{L. Wos} et al., Automated reasoning: introduction and applications. Incl. 1 disk. 2nd ed. New York, NY: McGraw-Hill (1992; Zbl 0820.68116)
Veroff, Robert; Wos, Larry The linked inference principle. I: The formal treatment. (English) Zbl 0754.68102 J. Autom. Reasoning 8, No. 2, 213-274 (1992). Reviewer: N.Zamov (Kazan’) MSC: 68T15 PDFBibTeX XMLCite \textit{R. Veroff} and \textit{L. Wos}, J. Autom. Reasoning 8, No. 2, 213--274 (1992; Zbl 0754.68102) Full Text: DOI
Wos, Larry The problem of demodulating across argument and literal boundaries. (English) Zbl 0783.68111 J. Autom. Reasoning 9, No. 3, 407-408 (1992). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 9, No. 3, 407--408 (1992; Zbl 0783.68111) Full Text: DOI
Wos, Larry The problem of demodulator adjunction. (English) Zbl 0781.68104 J. Autom. Reasoning 9, No. 2, 289-290 (1992). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 9, No. 2, 289--290 (1992; Zbl 0781.68104) Full Text: DOI
Wos, Larry The problem of demodulation during inference rule application. (English) Zbl 0784.68080 J. Autom. Reasoning 9, No. 1, 141-143 (1992). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 9, No. 1, 141--143 (1992; Zbl 0784.68080) Full Text: DOI
McCune, William; Wos, Larry Experiments in automated deduction with condensed detachment. (English) Zbl 0925.68402 Kapur, D. (ed.), Automated deduction - CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15–18, 1992. Berlin: Springer. Lect. Notes Comput. Sci. 607, 209-223 (1992). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{W. McCune} and \textit{L. Wos}, Lect. Notes Comput. Sci. 607, 209--223 (1992; Zbl 0925.68402)
McCune, William; Wos, Larry Application of automated deduction to the search for single axioms for exponent groups. (English) Zbl 0925.20002 Voronkov, A. (ed.), Logic programming and automated reasoning. International conference, LPAR ’92, St. Peterburg, Russia, July 15–20, 1992. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 624, 131-136 (1992). MSC: 20A05 20-04 68T15 68N17 20F50 20E10 PDFBibTeX XMLCite \textit{W. McCune} and \textit{L. Wos}, Lect. Notes Comput. Sci. 624, 131--136 (1992; Zbl 0925.20002)
Wos, Larry; McCune, William The application of automated reasoning to questions in mathematics and logic. (English) Zbl 0997.03500 Ann. Math. Artif. Intell. 5, No. 2-4, 321-370 (1992). MSC: 03B35 03-04 68T15 PDFBibTeX XMLCite \textit{L. Wos} and \textit{W. McCune}, Ann. Math. Artif. Intell. 5, No. 2--4, 321--370 (1992; Zbl 0997.03500) Full Text: DOI
Wos, Larry The problem of choosing the type of subsumption to use. (English) Zbl 0733.68077 J. Autom. Reasoning 7, No. 3, 435-438 (1991). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 7, No. 3, 435--438 (1991; Zbl 0733.68077) Full Text: DOI
Wos, Larry Basic research problems: The problem of choosing the representation, inference rule, and strategy. (English) Zbl 0733.68076 J. Autom. Reasoning 7, No. 4, 631-634 (1991). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 7, No. 4, 631--634 (1991; Zbl 0733.68076) Full Text: DOI
McCune, William; Wos, Larry The absence and the presence of fixed point combinators. (English) Zbl 0731.03012 Theor. Comput. Sci. 87, No. 1, 221-228 (1991). Reviewer: G.Mints (Stanford) MSC: 03B40 03-04 68T15 PDFBibTeX XMLCite \textit{W. McCune} and \textit{L. Wos}, Theor. Comput. Sci. 87, No. 1, 221--228 (1991; Zbl 0731.03012) Full Text: DOI
Wos, Larry; McCune, William Automated theorem proving and logic programming: A natural symbiosis. (English) Zbl 0736.68072 J. Logic Program. 11, No. 1, 1-53 (1991). Reviewer: R.Horsch (Markdorf) MSC: 68T15 68N17 PDFBibTeX XMLCite \textit{L. Wos} and \textit{W. McCune}, J. Log. Program. 11, No. 1, 1--53 (1991; Zbl 0736.68072) Full Text: DOI
Wos, L.; Winker, S.; McCune, W.; Overbeek, R.; Lusk, E.; Stevens, R. Automated reasoning contributes to mathematics and logic. (English) Zbl 1509.68326 Stickel, Mark E. (ed.), Automated deduction – CADE-10. 10th international conference, Kaiserslautern, Germany, July 24–27, 1990. Proceedings. Berlin etc.: Springer-Verlag. Lect. Notes Comput. Sci. 449, 485-499 (1990). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{L. Wos} et al., Lect. Notes Comput. Sci. 449, 485--499 (1990; Zbl 1509.68326) Full Text: DOI
Wos, Larry The problem of finding a semantic strategy for focusing inference rules. (English) Zbl 0702.68093 J. Autom. Reasoning 6, No. 3, 337-339 (1990). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 6, No. 3, 337--339 (1990; Zbl 0702.68093) Full Text: DOI
Wos, Larry Meeting the challenge of fifty years of logic. (English) Zbl 0697.68091 J. Autom. Reasoning 6, No. 2, 213-232 (1990). MSC: 68T15 03-03 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 6, No. 2, 213--232 (1990; Zbl 0697.68091) Full Text: DOI
Wos, Larry The problem of finding an inference rule for set theory. (English) Zbl 0679.68178 J. Autom. Reasoning 5, No. 1, 93-95 (1989). MSC: 68T15 68T20 03B35 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 5, No. 1, 93--95 (1989; Zbl 0679.68178) Full Text: DOI
Wos, Larry The problem of determining the size of a complete set of reductions. (English) Zbl 0679.68177 J. Autom. Reasoning 5, No. 2, 235-237 (1989). MSC: 68T15 68T20 03B35 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 5, No. 2, 235--237 (1989; Zbl 0679.68177) Full Text: DOI
Wos, Larry The problem of guaranteeing the existence of a complete set of reductions. (English) Zbl 0679.68176 J. Autom. Reasoning 5, No. 3, 399-401 (1989). Reviewer: S.Gottwald MSC: 68T15 68T20 03B35 PDFBibTeX XMLCite \textit{L. Wos}, J. Autom. Reasoning 5, No. 3, 399--401 (1989; Zbl 0679.68176) Full Text: DOI
Wos, Larry Automated reasoning: 33 research problems. (English) Zbl 0663.68102 Englewood Cliffs, NJ: Prentice Hall. XIII, 319 p.; $ 15.20 (1988). Reviewer: C.H.Kevorchian MSC: 68T15 68-02 PDFBibTeX XMLCite \textit{L. Wos}, Automated reasoning: 33 research problems. Englewood Cliffs, NJ: Prentice Hall (1988; Zbl 0663.68102)
Wos, Larry; McCune, William Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs. (English) Zbl 0656.68103 Automated deduction, Proc. 9th Int. Conf., Argonne/Ill. 1988, Lect. Notes Comput. Sci. 310, 714-729 (1988). Reviewer: G.Mints MSC: 68T15 03B40 03B35 PDFBibTeX XML
McCune, William; Wos, Larry Erratum to “A case study in automated theorem proving: finding sages in combinatory logic”. (English) Zbl 0652.68106 J. Autom. Reasoning 4, No. 1, 110-111 (1988). MSC: 68T15 03B40 03B35 PDFBibTeX XMLCite \textit{W. McCune} and \textit{L. Wos}, J. Autom. Reasoning 4, No. 1, 110--111 (1988; Zbl 0652.68106)
McCune, William; Wos, Larry A case study in automated theorem proving: Finding sages in combinatory logic. (English) Zbl 0636.68121 J. Autom. Reasoning 3, 91-107 (1987). Reviewer: J.Zlatuska MSC: 68T15 03B40 03B35 PDFBibTeX XMLCite \textit{W. McCune} and \textit{L. Wos}, J. Autom. Reasoning 3, 91--107 (1987; Zbl 0636.68121) Full Text: DOI
Wos, L.; McCune, W. Negative paramodulation. (English) Zbl 0643.68143 Automated deduction, Proc. 8th Int. Conf., Oxford/Engl. 1986, Lect. Notes Comput. Sci. 230, 229-239 (1986). MSC: 68T15 68W30 PDFBibTeX XML
Wos, L.; Pereira, Fernando; Hong, Robert; Boyer, Robert S.; Moore, J. Strother; Bledsoe, W. W.; Henschen, L. J.; Buchanan, Bruce G.; Wrightson, Graham; Green, Cordell An overview of automated reasoning and related fields. (English) Zbl 0614.68068 J. Autom. Reasoning 1, 5-48 (1985). MSC: 68T15 68-01 68T20 68Q60 68-02 68T99 PDFBibTeX XMLCite \textit{L. Wos} et al., J. Autom. Reasoning 1, 5--48 (1985; Zbl 0614.68068)
Wos, L. Automated reasoning. (English) Zbl 0593.68063 Am. Math. Mon. 92, 85-92 (1985). Reviewer: J.Chrz MSC: 68T15 03B35 68T20 03-01 03-02 68-01 68-02 PDFBibTeX XMLCite \textit{L. Wos}, Am. Math. Mon. 92, 85--92 (1985; Zbl 0593.68063) Full Text: DOI
Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim Automated reasoning. Introduction and applications. (English) Zbl 0674.68057 Englewood Cliffs, New Jersey 07632: Prentice-Hall, Inc. XIV, 482 p. (1984). MSC: 68T15 68-01 94C10 PDFBibTeX XML
Wos, L.; Winker, S. Open questions solved with the assistance of AURA. (English) Zbl 0566.68076 Automated theorem proving, Proc. Spec. Sess., 89th Meet. Am. Math. Soc., Denver/Colo. 1983, Contemp. Math. 29, 73-88 (1984). MSC: 68T15 PDFBibTeX XML
Wos, L. Solving open questions with an automated theorem-proving program. (Russian) Zbl 0564.68063 Kibern. Sb., Nov. Ser. 21, 235-263 (1984). MSC: 68T15 20M99 94C10 03B35 68T20 PDFBibTeX XMLCite \textit{L. Wos}, Kibern. Sb., Nov. Ser. 21, 235--263 (1984; Zbl 0564.68063)
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
Siekmann, Jörg (ed.); Wrightson, Graham (ed.) [Wos, L.; Henschen, L.; Binkley, R. W.; Clark, R. L.; Maslov, S. Yu.; Slagle, J. R.; Robinson, G. A.; Carson, D. F.; Shalla, L.; Andrews, P. B.; Loveland, D. W.; Robinson, J. A.; de Bruijn, N. G.; Guard, J. R.; Oglesby, F. C.; Bennett, J. H.; Settle, L. G.; Kowalski, R.; Hayes, P. J.; Morris, J. B.; Prawitz, D.; Anderson, R.; Bledsoe, W. W.; Chang, C. L.; Knuth, D. E.; Bendix, P. B.; Allen, J.; Luckham, D.; Tsejtin, G. S.; Davydov, G. V.; Mints, G. E.; Orevkov, V. P.; Slisenko, A. O.; Kuehner, D.] Automation of reasoning. 2: Classical papers on computational logic 1967- 1970. (English) Zbl 0567.03002 Symbolic Computation. Artificial Intelligence. Berlin etc.: Springer- Verlag. XII, 637 p. DM 108.00 (1983). Reviewer: N.Curteanu MSC: 03-06 68-06 03B35 68T15 01A75 PDFBibTeX XML
[Guiho, G.; McDermott, J.; Colmerrauer, A.; Gazdar, G.; Wos, L.; Mitchell, T. M.; Samuel, A. L.; Barstow, D.; Rosenschein, S.; Mackworth, A.; Kowalsky, R.; Gallaire, H.; Yokoi, T.; Dewar, R.; Nilsson, N. J.; Cook, S. B.; Kay, A. C.; Duchin, F.; Boden, M. A.; Chamot, D.; Reiter, R.; King, J. J.; Mylopoulos, J.; Webber, B. L.] Proceedings of the Eighth International Joint Conference on Artificial Intelligence (IJCAI-83), 8-12 August 1983, Karlsruhe, West Germany. Vols. 1, 2. Sponsored by: International Joint Conferences on Artificial Intelligence, Inc. Cosponsored by: Gesellschaft für Informatik; Society for the Study of Artificial Intelligence and the Simulation of Behaviour; Nederlandse Vereniging voor Kunstmatige Intelligentie. (German) Zbl 0536.68074 Los Altos, California: International Joint Conferences on Artificial Intelligence. William Kaufmann, Inc. XIX, 1208 p., I-15 £46.95 (1983). Reviewer: N.Curteanu MSC: 68Txx 68-06 68-02 68T50 68W30 68T05 68T10 68T15 68T20 68T99 68Q55 68N20 PDFBibTeX XML
Wos, L. Solving open questions with an automated theorem-proving program. (English) Zbl 0481.68090 Automated deduction, 6th Conf., New York 1982, Lect. Notes Comput. Sci. 138, 1-31 (1982). MSC: 68T15 03B35 94C10 68T20 20M99 PDFBibTeX XML
Winker, S. K.; Wos, L.; Lusk, E. L. Semigroups, antiautomorphisms, and involutions: A computer solution to an open problem. I. (English) Zbl 0517.20041 Math. Comput. 37, 533-545 (1981). MSC: 20M10 68T15 PDFBibTeX XMLCite \textit{S. K. Winker} et al., Math. Comput. 37, 533--545 (1981; Zbl 0517.20041) Full Text: DOI
Wos, L.; Overbeek, R.; Henschen, L. Hyperparamodulation: A refinement of paramodulation. (English) Zbl 0441.68114 Automated deduction, 5th Conf., Les Arcs/France 1980, Lect. Notes Comput. Sci. 87, 208-219 (1980). MSC: 68T15 PDFBibTeX XML
Overbeek, R.; McCharen, J.; Wos, L. Complexity and related enhancements for automated theorem-proving programs. (English) Zbl 0336.68037 Comput. Math. Appl. 2, 1-16 (1976). MSC: 68T15 PDFBibTeX XMLCite \textit{R. Overbeek} et al., Comput. Math. Appl. 2, 1--16 (1976; Zbl 0336.68037) Full Text: DOI
Henschen, L.; Wos, L. Unit refutations and Horn sets. (English) Zbl 0296.68093 J. Assoc. Comput. Mach. 21, 590-605 (1974). MSC: 68T15 PDFBibTeX XMLCite \textit{L. Henschen} and \textit{L. Wos}, J. Assoc. Comput. Mach. 21, 590--605 (1974; Zbl 0296.68093) Full Text: DOI
Henschen, L.; Wos, L. A theorem-proving language for experimentation. (English) Zbl 0279.68017 Commun. ACM 17, 308-314 (1974). MSC: 68N01 68T15 68T10 PDFBibTeX XMLCite \textit{L. Henschen} and \textit{L. Wos}, Commun. ACM 17, 308--314 (1974; Zbl 0279.68017) Full Text: DOI
Robinson, G.; Wos, L. Paramodulation and theorem-proving in first-order theories with equality. (English) Zbl 0219.68047 Machine Intell. 4, 135-150 (1969). MSC: 68T15 PDFBibTeX XMLCite \textit{G. Robinson} and \textit{L. Wos}, Mach. Intell. 4, 135--150 (1969; Zbl 0219.68047)