Automated Deduction in Geometry
8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Papers
Published on 10. November 2011
X, 259 pages
978-3-642-25070-5 (ISBN)
Description
This book constitutes the thoroughly refereed post-workshop proceedings of the 8th International Workshop on Automated Deduction in Geometry, ADG 2010, held in Munich, Germany in July 2010.
The 13 revised full papers presented were carefully selected during two rounds of reviewing and improvement from the lectures given at the workshop. Topics addressed by the papers are incidence geometry using some kind of combinatoric argument; computer algebra; software implementation; as well as logic and proof assistants.
More details
Other editions
Additional editions
Pascal Schreck | Julien Narboux | Jürgen Richter-Gebert
Automated Deduction in Geometry
8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Papers
Book
11/2011
Springer
€53.49
Shipment within 7-9 days
Content
- Intro
- Title
- Preface
- Organization
- Table of Contents
- Cancellation Patterns in Automatic Geometric Theorem Proving
- Introduction
- Definitions: Theorems and Proving Techniques
- The Binomial Proving Method
- How to Represent a Theorem?
- The Ceva-Menelaus Proving Method
- Modeling Theorems by Ceva-Menelaus Constructions
- Fractions, Groups and Graphs
- The Base Graph
- Triangles in Ceva-Menelaus Proofs Are Triangles in
- Biquadratic Fractions Are Quadrangles in
- Chains of Quadrangles
- Equivalence!
- How to Derive a Ceva-Menelaus Proof from a Binomial Proof
- From a Ceva-Menelaus Proof to a Binomial Proof
- Conclusion
- References
- Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL
- Introduction
- On Nonstandard Analysis in Isabelle
- Nonstandard Numbers
- Two New Relations on the Hyperreals
- The Harthong-Reeb System
- From HR to the (Limited) Hyperreals and Back
- Arithmetizing and Mechanizing Euler's Method
- Formally Verifying an Arithmetization at the Scale
- Interpreting the Arithmetization at the Scale
- A Verified Arithmetization of the Straight Line
- Discussion
- Conclusion and Further Work
- References
- A Formalization of Grassmann-Cayley Algebra in Coq and Its Application to Theorem Proving in Projective Geometry
- Introduction
- Formal Grassmann-Cayley Algebra
- The Underlying Vector Space
- The Join Product
- The Meet Product
- Data-Structures
- Representing the Vector Space Kn
- Representing the Algebra Gn
- Join Product
- Meet Product
- Duality
- Theorem Proving in Projective Geometry
- Modeling the Geometry of Incidence
- Automating Proofs
- Conclusion
- References
- Automatic Calculation of Plane Loci Using Gr\"{o}bner Bases and Integration into a Dynamic Geometry System
- Introduction
- Calculating Loci with Gröbner Bases
- The Algorithm
- Example
- Integration of Locus Computation in JSXGraph
- JSXGraph
- Calculating Loci with JSXGraph
- An Idea for Speed Improvements
- Conclusion
- References
- Proof Documents for Automated Origami Theorem Proving
- Introduction
- Motivation
- State of the Art of Origami Theorem Proving
- Reasoning about Origami
- Algorithm of Origami Construction and Proving
- A Simple Example of Construction
- Fold Principle
- Program of Construction
- Program of Proving
- Method of Proving
- Overview
- Need for Proof Document
- Local Geometrical Inference
- Transformation to Logical Formula
- Elimination of Unnecessary Predicates
- Forming Equivalence and Collinear Relations
- Algebraic Manipulation
- Proof Document
- Structure of Proof Document
- Program, Prover Computation and Result Sections
- Geometrical Reasoning Section
- Algebraic Transformation Section
- Conclusion
- References
- The Midpoint Locus of a Triangle in a Corner
- Introduction
- Setting up the Problem
- Approximating the Locus with a Graphic-Numeric Method
- Solving Algebraically
- Visualizing the Algebraic Surface
- The Rest of the Boundary
- Inverse Problems
- Summary and Open Questions
- Appendix: Mathematica Code
- References
- Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry
- Introduction
- Chasles, Pascal, Brianchon
- Desargue's Theorem
- Desargue's in Cevian Case
- The 3 Chords Theorem
- The Dual of 3 Chords Theorem
- The 3 Circles Theorem
- The 4 Circles Theorem
- Automatization
- Conclusion
- References
- What Is a Line ?
- Introduction: What Is a Line ?
- Pappus Geometry: A Summary
- Three Times Constrained Conics
- Conditions, or Vector-Based Constraints for Conics
- Examples of Non Naive Lines
- Circles through One Fixed Point
- Orthogonal Circles
- Poincaré Half Circles Are Lines
- Other Circles
- Some Parabolas Are Lines
- Conics through Three Fixed Points Are Lines
- Playing with Some Theorems
- Proof of the Three Circles Theorem
- The Four Circles Theorem
- A Butterfly Theorem
- What Is a Point ?
- Variants: A Zoo of Planes
- Conclusion
- References
- On One Method of Proving Inequalities in Automated Way
- Introduction
- Basic Method
- Parametrization of n-gons
- Proving Inequalities by Introduction of Auxiliary Polynomials
- Concluding Remarks
- References
- Thousands of Geometric Problems for Geometric Theorem Provers (TGTP)
- Introduction
- TGTP
- Realm
- The Web Interface
- The List of Problems
- Queries
- Performance Information
- Common File Format for Conjectures
- Future Work
- Conclusions
- References
- An Investigation of Hilbert's Implicit Reasoning through Proof Discovery in Idle-Time
- Introduction
- Declarative Formalisation
- HOL Light
- Incidence Reasoning
- Incidence Rules
- Incidence and Pasch's Axiom
- Idle-Time Discovery
- Overview of the System
- Analysing Hilbert's Proofs
- Theorem 4
- Theorem 5
- Conclusion and Further Work
- References
- A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
- Introduction
- Background
- ArgoCLP Proof Procedures
- Basic Proof Procedure
- Improved Proof Procedure
- Techniques That Do Not Preserve Completeness
- ArgoCLP Implementation
- Applications
- Related Work
- Conclusions and Further Work
- References
- Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method
- Introduction
- Mass Point Geometry
- Mass Point Geometry Preliminaries
- Basic Propositions of Mass Point Geometry
- Mass Point Method
- Introductory Examples
- The Hilbert Intersection Point Statesments
- The Algorithm and Its Features
- Implementing the Algorithm MPM in Maple
- Running Examples
- Further Discussion
- The Complex Mass Point Geometry
- The Basic Idea
- The Properties of the Complex Mass Point Geometry
- Complex Mass Point Method
- Introductory Examples
- Some Features
- The Linear Constructive Geometry Statements
- The Algorithm Complex Mass Point Method
- Implementing the Algorithm CMPM in Maple
- Running Examples
- Experimental Results and Conclusions
- Experimental Results
- Conclusions and Future Work
- References
- Author Index
