Coghetto, Roland; Grabowski, Adam Tarski geometry axioms. IV: Right angle. (English) Zbl 1422.51002 Formaliz. Math. 27, No. 1, 75-85 (2019). MSC: 51A05 51M04 03B35 PDFBibTeX XMLCite \textit{R. Coghetto} and \textit{A. Grabowski}, Formaliz. Math. 27, No. 1, 75--85 (2019; Zbl 1422.51002) Full Text: DOI
Kellison, Ariel; Bickford, Mark; Constable, Robert Implementing Euclid’s straightedge and compass constructions in type theory. (English) Zbl 1479.03009 Ann. Math. Artif. Intell. 85, No. 2-4, 175-192 (2019). Reviewer: Marco Benini (Buccinasco) MSC: 03B35 03F55 51M04 03B38 PDFBibTeX XMLCite \textit{A. Kellison} et al., Ann. Math. Artif. Intell. 85, No. 2--4, 175--192 (2019; Zbl 1479.03009) Full Text: DOI
Coghetto, Roland; Grabowski, Adam Tarski geometry axioms. III. (English) Zbl 1401.51003 Formaliz. Math. 25, No. 4, 289-313 (2017). MSC: 51A05 03B35 PDFBibTeX XMLCite \textit{R. Coghetto} and \textit{A. Grabowski}, Formaliz. Math. 25, No. 4, 289--313 (2017; Zbl 1401.51003) Full Text: DOI
Plaisted, David A. History and prospects for first-order automated deduction. (English) Zbl 1465.03055 Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 3-28 (2015). MSC: 03B35 03-03 68-03 68V15 PDFBibTeX XMLCite \textit{D. A. Plaisted}, Lect. Notes Comput. Sci. 9195, 3--28 (2015; Zbl 1465.03055) Full Text: DOI
Fitelson, Branden Gibbard’s collapse theorem for the indicative conditional: an axiomatic approach. (English) Zbl 1383.03011 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, 181-188 (2013). MSC: 03A05 PDFBibTeX XMLCite \textit{B. Fitelson}, Lect. Notes Comput. Sci. 7788, 181--188 (2013; Zbl 1383.03011) Full Text: DOI
Fitelson, Branden; Zalta, Edward N. Steps toward a computational metaphysics. (English) Zbl 1121.03009 J. Philos. Log. 36, No. 2, 227-247 (2007). MSC: 03A05 03B35 68T15 PDFBibTeX XMLCite \textit{B. Fitelson} and \textit{E. N. Zalta}, J. Philos. Log. 36, No. 2, 227--247 (2007; Zbl 1121.03009) Full Text: DOI
Hedman, Shawn A first course in logic. An introduction to model theory, proof theory, computability, and complexity. (English) Zbl 1095.03001 Oxford Texts in Logic 1. Oxford: Oxford University Press (ISBN 0-19-852981-3/hbk; 0-19-852980-5/pbk). xx, 431 p. (2004). Reviewer: Victor V. Pambuccian (Phoenix) MSC: 03-01 PDFBibTeX XMLCite \textit{S. Hedman}, A first course in logic. An introduction to model theory, proof theory, computability, and complexity. Oxford: Oxford University Press (2004; Zbl 1095.03001)
Karpenko, A. S. (ed.) Proceedings of the scientific research seminar of the Logic Center of the Institute of Philosophy RAS. 2000–2001. No. XV. (Trudy nauchno-issledovatel’skogo seminara Logicheskogo Tsentra Instituta Filosofii RAN. 2000–2001. Vyp. XV.) (Russian) Zbl 0989.00031 Trudy Nauchno-Issledovatel’skogo Seminara Logicheskogo Tsentra Instituta Filosofii RAN. 15. Moskva: Rossijskaya Akademiya Nauk, Institut Filosofii. 127 p. (2001). MSC: 00B25 03-06 PDFBibTeX XMLCite \textit{A. S. Karpenko} (ed.), Trudy nauchno-issledovatel'skogo seminara Logicheskogo Tsentra Instituta Filosofii RAN. 2000--2001. Vyp. XV (Russian). Moskva: Rossijskaya Akademiya Nauk, Institut Filosofii (2001; Zbl 0989.00031)
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
Burris, Stanley N. Logic for mathematics and computer science. (English) Zbl 0959.03002 Upper Saddle River, NJ: Prentice Hall. xix, 420 p. (1998). Reviewer: Martin Hofmann (Edinburgh) MSC: 03-01 03B05 03B10 03B35 68Q42 68T15 03-03 PDFBibTeX XMLCite \textit{S. N. Burris}, Logic for mathematics and computer science. Upper Saddle River, NJ: Prentice Hall (1998; Zbl 0959.03002)
McCune, William; Padmanabhan, R. Automated deduction in equational logic and cubic curves. (English) Zbl 0921.03011 Lecture Notes in Computer Science 1095. Lecture Notes in Artificial Intelligence. Berlin: Springer-Verlag. ix, 231 p. DM 54.00; öS 394.20; sFr. 48.00 (1996). MSC: 03B35 68T15 03-02 68-02 03C05 08-04 14-04 14Q05 14H45 PDFBibTeX XMLCite \textit{W. McCune} and \textit{R. Padmanabhan}, Automated deduction in equational logic and cubic curves. Berlin: Springer-Verlag (1996; Zbl 0921.03011) Full Text: DOI
Jech, Thomas OTTER experiments in a system of combinatory logic. (English) Zbl 0822.03011 J. Autom. Reasoning 14, No. 3, 413-426 (1995). MSC: 03B40 68T15 03-04 PDFBibTeX XMLCite \textit{T. Jech}, J. Autom. Reasoning 14, No. 3, 413--426 (1995; Zbl 0822.03011) Full Text: DOI arXiv
McCune, William W. Single axioms for the left group and right group calculi. (English) Zbl 0804.03006 Notre Dame J. Formal Logic 34, No. 1, 132-139 (1993). MSC: 03B35 03-04 20-04 68T15 20E05 PDFBibTeX XMLCite \textit{W. W. McCune}, Notre Dame J. Formal Logic 34, No. 1, 132--139 (1993; Zbl 0804.03006) Full Text: DOI
Quaife, Art Automated development of fundamental mathematical theories. (English) Zbl 0773.03010 Automated Reasoning Series. 2. Dordrecht: Kluwer Academic Publishers. xviii, 271 p. (1992). Reviewer: H.J.Ohlbach (Saarbrücken) MSC: 03B35 03-02 68T15 PDFBibTeX XMLCite \textit{A. Quaife}, Automated development of fundamental mathematical theories. Dordrecht: Kluwer Academic Publishers (1992; Zbl 0773.03010)
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 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