Formalizing Pick's theorem in Isabelle/HOL

DOI10.1007/978-3-031-66997-2_7MaRDI QIDQ6648161

Katherine Kosaian, Sage Binder

Publication date: 4 December 2024

zbMATH Keywords

geometryIsabelle/HOLformalizationPick's theorem

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites Work

• Title not available (Why is that?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Formal verification of a geometry algorithm: A quest for abstract views and symmetry in coq proofs
• The foundation of a generic theorem prover
• The HOL Light theory of Euclidean space
• A formal proof of Pick's Theorem
• Without Loss of Generality
• The Jordan Curve Theorem, Formally and Informally
• Formal Study of Plane Delaunay Triangulation
• Geometrical aspects of number theory.

This page was built for publication: Formalizing Pick's theorem in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6648161)