Automated Deduction in Geometry

DOI10.1007/11615798MaRDI QIDQ5493316zbMATH OpenOpenAlexFDO

Authors Laura I. Meikle, Jacques D. Fleuriot

Publication date 20 October 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11615798

Mathematics Subject Classification ID

Computer graphics; computational geometry (digital and algorithmic aspects) (68U05)

Recommendations

• scientific article; zbMATH DE number 1863395
• Automatted geometry theorem proving
• A CASE STUDY IN ALGORITHM ENGINEERING FOR GEOMETRIC COMPUTING
• Geometric theorem proving by integrated logical and algebraic reasoning
• An invitation to analysing geometric problems by executing pseudodivisions

Cited in

(21)

• Automated reasoning in differential geometry and mechanics using the characteristic set method. II: Mechanical theorem proving
• Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
• A verified ODE solver and the Lorenz attractor
• Formalization of the Poincaré disc model of hyperbolic geometry
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• Design and formal proof of a new optimal image segmentation program with hypermaps
• scientific article; zbMATH DE number 1601215 (Why is no real title available?)
• Formal proof in Coq and derivation of an imperative program to compute convex hulls
• An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
• scientific article; zbMATH DE number 4155933 (Why is no real title available?)
• scientific article; zbMATH DE number 3926284 (Why is no real title available?)
• Formal specification and proofs for the topology and classification of combinatorial surfaces
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• scientific article; zbMATH DE number 6984221 (Why is no real title available?)
• scientific article; zbMATH DE number 2160466 (Why is no real title available?)
• scientific article; zbMATH DE number 1863395 (Why is no real title available?)
• Verification of Closest Pair of Points Algorithms
• Mechanical Theorem Proving in Tarski’s Geometry
• Combining Isabelle and QEPCAD-B in the Prover’s Palette
• Mechanical geometry theorem proving based on Gröbner bases
• Nonrealizability proofs in computational geometry

Describes a project that uses

Uses Software

• Isabelle/HOL
• HOL

This page was built for publication: Automated Deduction in Geometry

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