×

Found 82 Documents (Results 1–82)

Mathesis universalis and homotopy type theory. (English) Zbl 1469.03035

Centrone, Stefania (ed.) et al., Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. Cham: Springer. Synth. Libr. 412, 13-36 (2019).
MSC:  03B38 55U40
PDFBibTeX XMLCite
Full Text: DOI

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).
MSC:  68T15 51M05 51N20
PDFBibTeX XMLCite

Formalizing some “small” finite models of projective geometry in Coq. (English) Zbl 1515.68349

Fleuriot, Jacques (ed.) et al., Artificial intelligence and symbolic computation. 13th international conference, AISC 2018, Suzhou, China, September 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11110, 54-69 (2018).
PDFBibTeX XMLCite
Full Text: DOI HAL

Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs. (English) Zbl 1518.68417

Fischer, Bernd (ed.) et al., Theoretical aspects of computing – ICTAC 2018. 15th international colloquium, Stellenbosch, South Africa, October 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11187, 3-10 (2018).
MSC:  68V20 52B70
PDFBibTeX XMLCite
Full Text: DOI arXiv

Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13–17, 2018. Proceedings. (English) Zbl 1392.68030

Lecture Notes in Computer Science 11006. Lecture Notes in Artificial Intelligence. Cham: Springer (ISBN 978-3-319-96811-7/pbk; 978-3-319-96812-4/ebook). xii, 287 p. (2018).
MSC:  68-06 68Txx 00B25
PDFBibTeX XMLCite
Full Text: DOI

Deepalgebra – an outline of a program. (English) Zbl 1367.68247

Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 1-8 (2017).
MSC:  68T15 14-04
PDFBibTeX XMLCite
Full Text: DOI arXiv

Certified universal gathering in \(\mathbb {R}^2\) for oblivious mobile robots. (English) Zbl 1393.68163

Gavoille, Cyril (ed.) et al., Distributed computing. 30th international symposium, DISC 2016, Paris, France, September 27–29, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-53425-0/pbk; 978-3-662-53426-7/ebook). Lecture Notes in Computer Science 9888, 187-200 (2016).
MSC:  68T40 68M14 68U05
PDFBibTeX XMLCite
Full Text: DOI arXiv

Wang tile modeling of wall patterns. (English) Zbl 1401.68348

Dobashi, Yoshinori (ed.) et al., Mathematical progress in expressive image synthesis III. Selected and extended results from the symposium MEIS 2015, Fukuoka, Japan, September 25–27, 2015. Singapore: Springer (ISBN 978-981-10-1075-0/hbk; 978-981-10-1076-7/ebook). Mathematics for Industry 24, 71-81 (2016).
MSC:  68U05 68U10
PDFBibTeX XMLCite
Full Text: DOI

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
Full Text: DOI

Hypermap specification and certified linked implementation using orbits. (English) Zbl 1416.68160

Klein, Gerwin (ed.) et al., Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8558, 242-257 (2014).
MSC:  68T15 68Q60 68Q65 68U05
PDFBibTeX XMLCite
Full Text: DOI

Abstraction and invariance for algebraically indexed types. (English) Zbl 1301.68183

Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’13, Rome, Italy, January 23–25, 2013. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1832-7). 87-100 (2013).
MSC:  68Q65 68N18 68N30 68T15 68U05
PDFBibTeX XMLCite
Full Text: DOI Link

Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP ’13, Boston, MA, USA, September 25–27, 2013. (English) Zbl 1282.68050

ACM SIGPLAN Notices 48, No. 9. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2326-0). xii, 469 p. (2013).
MSC:  68-06 68N18 00B25
PDFBibTeX XMLCite
Full Text: DOI

From Tarski to Hilbert. (English) Zbl 1397.03019

Ida, Tetsuo (ed.) et al., Automated deduction in geometry. 9th international workshop, ADG 2012, Edinburgh, UK, September 17–19, 2012. Revised selected papers. Berlin: Springer (ISBN 978-3-642-40671-3/pbk). Lecture Notes in Computer Science 7993. Lecture Notes in Artificial Intelligence, 89-109 (2013).
MSC:  03B35 03B30 68T15
PDFBibTeX XMLCite
Full Text: DOI HAL

Formal proof in Coq and derivation of an imperative program to compute convex hulls. (English) Zbl 1396.68111

Ida, Tetsuo (ed.) et al., Automated deduction in geometry. 9th international workshop, ADG 2012, Edinburgh, UK, September 17–19, 2012. Revised selected papers. Berlin: Springer (ISBN 978-3-642-40671-3/pbk). Lecture Notes in Computer Science 7993. Lecture Notes in Artificial Intelligence, 71-88 (2013).
MSC:  68T15 52B55 68U05
PDFBibTeX XMLCite
Full Text: DOI HAL

Automated deduction in geometry. 9th international workshop, ADG 2012, Edinburgh, UK, September 17–19, 2012. Revised selected papers. (English) Zbl 1272.68023

Lecture Notes in Computer Science 7993. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-642-40671-3/pbk). ix, 193 p. (2013).
MSC:  68-06 68T15 00B25
PDFBibTeX XMLCite
Full Text: DOI

A combination of a dynamic geometry software with a proof assistant for interactive formal proofs. (English) Zbl 1294.68126

Aspinall, David (ed.) et al., Proceedings of the 9th international workshop on user interfaces for theorem provers (UITP10), Edinburgh, UK, July 15, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 285, 43-55 (2012).
MSC:  68T15 68U05 68U35
PDFBibTeX XMLCite
Full Text: DOI

Proceedings of the 9th international workshop on user interfaces for theorem provers (UITP10), Edinburgh, UK, July 15, 2010. (English) Zbl 1284.68005

Electronic Notes in Theoretical Computer Science 285. Amsterdam: Elsevier. 120 p., electronic only (2012).
MSC:  68-06 68T15 68U35 00B25
PDFBibTeX XMLCite
Full Text: Link

Intelligent computer mathematics. 11th international conference, AISC 2012, 19th symposium, Calculemus 2012, 5th international workshop, DML 2012, 11th international conference, MKM 2012, systems and projects, held as part of CICM 2012, Bremen, Germany, July 8–13, 2012. Proceedings. (English) Zbl 1245.68013

Lecture Notes in Computer Science 7362. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-642-31373-8/pbk). xviii, 473 p. (2012).
MSC:  68-06 68Txx 00B25
PDFBibTeX XMLCite
Full Text: DOI

A coherent logic based geometry theorem prover capable of producing formal and readable proofs. (English) Zbl 1252.68264

Schreck, Pascal (ed.) et al., Automated deduction in geometry. 8th international workshop, ADG 2010, Munich, Germany, July 22–24, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-25069-9/pbk). Lecture Notes in Computer Science 6877. Lecture Notes in Artificial Intelligence, 201-220 (2011).
MSC:  68T15 03B35
PDFBibTeX XMLCite
Full Text: DOI

Proof documents for automated origami theorem proving. (English) Zbl 1350.68235

Schreck, Pascal (ed.) et al., Automated deduction in geometry. 8th international workshop, ADG 2010, Munich, Germany, July 22–24, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-25069-9/pbk). Lecture Notes in Computer Science 6877. Lecture Notes in Artificial Intelligence, 78-97 (2011).
MSC:  68T15 51M15
PDFBibTeX XMLCite
Full Text: DOI

A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry. (English) Zbl 1350.68233

Schreck, Pascal (ed.) et al., Automated deduction in geometry. 8th international workshop, ADG 2010, Munich, Germany, July 22–24, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-25069-9/pbk). Lecture Notes in Computer Science 6877. Lecture Notes in Artificial Intelligence, 51-67 (2011).
MSC:  68T15 51A05 51A30
PDFBibTeX XMLCite
Full Text: DOI HAL

Formalization of Wu’s simple method in Coq. (English) Zbl 1350.68234

Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 71-86 (2011).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Automated deduction in geometry. 8th international workshop, ADG 2010, Munich, Germany, July 22–24, 2010. Revised selected papers. (English) Zbl 1227.68009

Lecture Notes in Computer Science 6877. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-642-25069-9/pbk). x, 259 p. (2011).
MSC:  68-06 68T15 00B25
PDFBibTeX XMLCite
Full Text: DOI

Proof assistant decision procedures for formalizing origami. (English) Zbl 1335.68230

Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 45-57 (2011).
MSC:  68T15 68W30
PDFBibTeX XMLCite
Full Text: DOI

Formalizing projective plane geometry in Coq. (English) Zbl 1302.68246

Sturm, Thomas (ed.) et al., Automated deduction in geometry. 7th international workshop, ADG 2008, Shanghai, China, September 22–24, 2008. Revised papers. Berlin: Springer (ISBN 978-3-642-21045-7/pbk). Lecture Notes in Computer Science 6301. Lecture Notes in Artificial Intelligence, 141-162 (2011).
MSC:  68T15 51N15
PDFBibTeX XMLCite
Full Text: DOI

Proof certificates for algebra and their application to automatic geometry theorem proving. (English) Zbl 1302.68242

Sturm, Thomas (ed.) et al., Automated deduction in geometry. 7th international workshop, ADG 2008, Shanghai, China, September 22–24, 2008. Revised papers. Berlin: Springer (ISBN 978-3-642-21045-7/pbk). Lecture Notes in Computer Science 6301. Lecture Notes in Artificial Intelligence, 42-59 (2011).
MSC:  68T15 13P10
PDFBibTeX XMLCite
Full Text: DOI Link

Automated deduction in geometry. 7th international workshop, ADG 2008, Shanghai, China, September 22–24, 2008. Revised papers. (English) Zbl 1214.68020

Lecture Notes in Computer Science 6301. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-642-21045-7/pbk). vii, 225 p. (2011).
MSC:  68-06 68T15 00B25
PDFBibTeX XMLCite
Full Text: DOI

Intelligent computer mathematics. 10th international conference, AISC 2010, 17th symposium, Calculemus 2010, and 9th international conference, MKM 2010, Paris, France, July 5–10, 2010. Proceedings. (English) Zbl 1194.68011

Lecture Notes in Computer Science 6167. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-642-14127-0/pbk). xv, 471 p. (2010).
MSC:  68-06 68Txx 00B25
PDFBibTeX XMLCite
Full Text: DOI

GeoThms – a web system for Euclidean constructive geometry. (English) Zbl 1278.68279

Autexier, Serge (ed.) et al., Proceedings of the 7th workshop on user interfaces for theorem provers (UITP 2006), Seattle, WA, USA, August 21, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 2, 35-48 (2007).
MSC:  68T15 68U35
PDFBibTeX XMLCite
Full Text: DOI

Mechanical theorem proving in Tarski’s geometry. (English) Zbl 1195.03019

Botana, Francisco (ed.) et al., Automated deduction in geometry. 6th international workshop, ADG 2006, Pontevedra, Spain, August 31–September 2, 2006. Revised papers. Berlin: Springer (ISBN 978-3-540-77355-9/pbk). Lecture Notes in Computer Science 4869. Lecture Notes in Artificial Intelligence, 139-156 (2007).
MSC:  03B35 51-04 68T15
PDFBibTeX XMLCite
Full Text: DOI Link

Automating coherent logic. (English) Zbl 1143.03332

Sutcliffe, Geoff (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2–6, 2005. Proceedings. Berlin: Springer (ISBN 978-3-540-30553-8/pbk). Lecture Notes in Computer Science 3835, 246-260 (2005).
MSC:  03B35 68T15
PDFBibTeX XMLCite
Full Text: DOI

A decision procedure for geometry in Coq. (English) Zbl 1099.68734

Slind, Konrad (ed.) et al., Theorem proving in higher order logics. 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14–17, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23017-3/pbk). Lecture Notes in Computer Science 3223, 225-240 (2004).
MSC:  68T15 03B35 51-04
PDFBibTeX XMLCite
Full Text: DOI

Theorem proving in higher order logics. 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14–17, 2004. Proceedings. (English) Zbl 1060.68005

Lecture Notes in Computer Science 3223. Berlin: Springer (ISBN 3-540-23017-3/pbk). viii, 337 p. (2004).
MSC:  68-06 00B25 68T15 03-06 03B35
PDFBibTeX XMLCite
Full Text: DOI

Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 – May 4, 2003. Revised selected papers. (English) Zbl 1052.68001

Lecture Notes in Computer Science 3085. Berlin: Springer (ISBN 3-540-22164-6/pbk). x, 409 p. (2004).
MSC:  68-06 68N30 00B25
PDFBibTeX XMLCite
Full Text: DOI

Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry. (English) Zbl 0985.68078

Richter-Gebert, Jürgen (ed.) et al., Automated deduction in geometry. 3rd international workshop, ADG 2000, Zürich, Switzerland, September 25-27, 2000. Revised papers. Berlin: Springer. Lect. Notes Comput. Sci. 2061, 306-323 (2001).
MSC:  68U05 03F55 03B35 68T15
PDFBibTeX XMLCite
Full Text: Link

Computer aided systems theory - EUROCAST 2001. A selection of papers from the 8th international workshop, Las Palmas de Gran Canaria, Spain, February 19–23, 2001. Revised papers. (English) Zbl 0977.00038

Lecture Notes in Computer Science. 2178. Berlin: Springer. xi, 670 p. (2001).
MSC:  00B25 68-06 93-06
PDFBibTeX XMLCite

Filter Results by …

Document Type

all top 5

Author

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software