Coghetto, Roland; Grabowski, Adam Tarski geometry axioms. V: Half-planes and planes. (English) Zbl 1540.68281 Formaliz. Math. 31, No. 1, 325-339 (2023). MSC: 68V20 51A05 51M04 PDFBibTeX XMLCite \textit{R. Coghetto} and \textit{A. Grabowski}, Formaliz. Math. 31, No. 1, 325--339 (2023; Zbl 1540.68281) Full Text: DOI OA License
Macke, Jaroslav; Sedlar, Jiri; Olsak, Miroslav; Urban, Josef; Sivic, Josef Learning to solve geometric construction problems from images. (English) Zbl 1485.68271 Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 167-184 (2021). MSC: 68U05 68T05 68T45 PDFBibTeX XMLCite \textit{J. Macke} et al., Lect. Notes Comput. Sci. 12833, 167--184 (2021; Zbl 1485.68271) Full Text: DOI arXiv
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
Narboux, Julien; Janičić, Predrag; Fleuriot, Jacques Computer-assisted theorem proving in synthetic geometry. (English) Zbl 1425.68377 Sitharam, Meera (ed.) et al., Handbook of geometric constraint systems principles. Boca Raton, FL: CRC Press. Discrete Math. Appl. (Boca Raton), 21-59 (2019). Reviewer: Victor V. Pambuccian (Glendale) MSC: 68T15 51M05 51N20 PDFBibTeX XMLCite \textit{J. Narboux} et al., in: Handbook of geometric constraint systems principles. Boca Raton, FL: CRC Press. 21--59 (2019; Zbl 1425.68377)
Song, Dan; Wang, Dongming; Chen, Xiaoyu Retrieving geometric information from images: the case of hand-drawn diagrams. (English) Zbl 1411.68135 Data Min. Knowl. Discov. 31, No. 4, 934-971 (2017). MSC: 68T10 62H35 PDFBibTeX XMLCite \textit{D. Song} et al., Data Min. Knowl. Discov. 31, No. 4, 934--971 (2017; Zbl 1411.68135) 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
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
Stojanović Đurđević, Sana; Narboux, Julien; Janičić, Predrag Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry. (English) Zbl 1327.68206 Ann. Math. Artif. Intell. 74, No. 3-4, 249-269 (2015). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{S. Stojanović Đurđević} et al., Ann. Math. Artif. Intell. 74, No. 3--4, 249--269 (2015; Zbl 1327.68206) Full Text: DOI HAL
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
Demri, Stéphane (ed.); Kapur, Deepak (ed.); Weidenbach, Christoph (ed.) 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. (English) Zbl 1293.68021 Lecture Notes in Computer Science 8562. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-319-08586-9/pbk). xxviii, 528 p. (2014). MSC: 68-06 68T15 00B25 PDFBibTeX XMLCite \textit{S. Demri} (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 (2014; Zbl 1293.68021) Full Text: DOI
Padmanabhan, Ranganathan; Veroff, Robert A geometric procedure with Prover9. (English) Zbl 1383.68080 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, 139-150 (2013). MSC: 68T15 14H52 14Q05 PDFBibTeX XMLCite \textit{R. Padmanabhan} and \textit{R. Veroff}, Lect. Notes Comput. Sci. 7788, 139--150 (2013; Zbl 1383.68080) Full Text: DOI
Padmanabhan, R.; McCune, W. Uniqueness of Steiner laws on cubic curves. (English) Zbl 1112.14067 Beitr. Algebra Geom. 47, No. 2, 543-557 (2006). MSC: 14Q05 14H52 14N05 20N15 51M15 68T15 PDFBibTeX XMLCite \textit{R. Padmanabhan} and \textit{W. McCune}, Beitr. Algebra Geom. 47, No. 2, 543--557 (2006; Zbl 1112.14067) Full Text: EuDML EMIS
Ioakimidis, N. I. Finite differences/elements in classical beam problems: Derivation of feasibility conditions under parametric inequality constraints with the help of Reduce and REDLOG. (English) Zbl 1031.74048 Comput. Mech. 27, No. 2, 145-153 (2001). MSC: 74S05 74S20 74K10 PDFBibTeX XMLCite \textit{N. I. Ioakimidis}, Comput. Mech. 27, No. 2, 145--153 (2001; Zbl 1031.74048) Full Text: DOI
López Mimbela, J. Alfredo (ed.); Neumann, Max (ed.); Rzedowski, Martha (ed.); Shapiro, Michael (ed.) 30th national congress of the Mexican Mathematical Society, Aguascalientes, México, September 28–October 2, 1997. Proceedings. (XXX congreso nacional de la Sociedad Matemática Mexicana, Aguascalientes, México, 1997. Memorias.) (English, Spanish) Zbl 0948.00025 Aportaciones Matemáticas. Comunicaciones. 22. México: Sociedad Matemática Mexicana. 364 p. (1998). MSC: 00B25 PDFBibTeX XMLCite \textit{J. A. López Mimbela} (ed.) et al., XXX congreso nacional de la Sociedad Matemática Mexicana, Aguascalientes, México, 1997. Memorias (Spanish). México: Sociedad Matemática Mexicana (1998; Zbl 0948.00025)
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
Padmanabhan, R.; McCune, W. Automated reasoning about cubic curves. (English) Zbl 0828.68110 Comput. Math. Appl. 29, No. 2, 17-26 (1995). Reviewer: J.R.Sendra (Madrid) MSC: 68T15 14Q05 PDFBibTeX XMLCite \textit{R. Padmanabhan} and \textit{W. McCune}, Comput. Math. Appl. 29, No. 2, 17--26 (1995; Zbl 0828.68110) 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 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
Quaife, Art Automated development of Tarski’s geometry. (English) Zbl 0683.68082 J. Autom. Reasoning 5, No. 1, 97-118 (1989). Reviewer: Ch.Fenske MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{A. Quaife}, J. Autom. Reasoning 5, No. 1, 97--118 (1989; Zbl 0683.68082) Full Text: DOI