Automated Deduction in Geometry
7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008, Revised Papers
Published on 3. May 2011
IX, 225 pages
978-3-642-21046-4 (ISBN)
Description
This book constitutes the thoroughly refereed post-workshop proceedings of the 7th International Workshop on Automated Deduction in Geometry, ADG 2008, held in Shanghai, China in September 2008. The 11 revised full papers presented were carefully reviewed and selected from numerous initial submissions for the workshop during two rounds of reviewing and improvement. The papers show the lively variety of topics and methods and the current applicability of automated deduction in geometry to different branches of mathematics such as discrete mathematics, combinatorics, and numerics; symbolic and numeric methods for geometric computation, and geometric constraint solving. Further issues are the design and implementation of geometry software, special-purpose tools, automated theorem provers - in short applications of ADG to mechanics, geometric modeling, CAGD/CAD, computer vision, robotics and education.
More details
Other editions
Additional editions
Thomas Sturm | Christoph Zengler
Automated Deduction in Geometry
7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008, Revised Papers
Book
05/2011
1st Edition
Springer
€53.49
Shipment within 5-7 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Contributed Papers
- Dynamical Systems of Simplices in Dimension Two or Three
- Introduction
- The General Problem
- The Case d=3
- The Case d=2
- Computational Aspects of the Proofs
- Standard Definitions and Results about Tetrahedra
- General Tetrahedra
- Isosceles Tetrahedra
- Deformation from T0 to T1 (d=3)
- Parameters and Notations
- Inequalities
- Solution of the Case d=3. Part 1
- Solution of the Case d=3. Part 2
- Taylor Series I
- Taylor Series II
- Proof of the Property (*)
- The Main Result in Dimension Three
- Sequence of Cyclic Quadrilaterals
- Degenerate Simplices
- A Particular Case
- About the Limit
- Solution of the Case d=2
- The Parameters
- Deformation from T0 to T1
- Convergence of the Triangles
- The Main Result in Dimension Two
- Conclusion
- References
- On the Design and Implementation of a Geometric Knowledge Base
- Introduction
- Motivation
- State of the Art
- Problem
- Representation of Geometric Knowledge Objects
- Identification of Knowledge Data Elements
- Formalization of Data Elements
- Structure Design within Knowledge Objects
- Modeling of the Structure for the Knowledge Base
- Analysis on the Structure for the Knowledge Base
- Representation of the Structure of the Knowledge Base
- Implementation of the Knowledge Base System
- Naming Objects in the Knowledge Base
- Browsing and Querying the Knowledge Base
- Conclusion and Future Work
- References
- Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
- Introduction
- Nullstellensatz Theorem and Gröbner Basis
- Division of Polynomials
- Gröbner Bases
- Buchberger's Algorithm and Certificates
- Reflexive Method to Verify Large Certificates in Proof Assistant
- Geometry Theorem Proving
- Conclusion
- References
- Multivariate Resultants in Bernstein Basis
- Introduction
- Preliminaries
- Multivariate Resultants and Projection Operators
- Macaulay-Style Approach
- Bézout/Cayley/Dixon-Style Approach
- Multivariate (Tensor-Product) Bernstein Bases
- An Analogue of Macaulay-Style Resultant Construction
- Bézout/Cayley/Dixon-Style Resultant Construction
- Unmixed Bernstein Basis Degrees
- Mixed Bernstein Basis Degrees
- Dixon Resultant
- Applications
- A Theorem on Drawing by Compass and Ruler
- Surface-Curve Intersection
- Geometric Benchmarks
- Conclusion and Future Work
- References
- Unique Factorization Domains in the Java Computer Algebra System
- Introduction
- Related Work
- Outline
- Introduction to JAS
- GCD Class Layout
- Design Overview
- Interface GcdRingElem
- Recursive Methods
- Conversion of Representation
- GCD Implementations
- Polynomial Remainder Sequences
- Modular Methods
- GCD Factory
- GCD Proxy
- GCD Performance
- Relative Algorithm Performance
- Comparison with other CAS
- Application Performance
- GCD Evaluation
- Factorization
- Class Layout
- Modular, Integer and Rational Coefficients
- Algebraic Number Coefficients
- Absolute Factorization
- Factor Factory
- Real Roots
- Real Algebraic Numbers
- Conclusions
- References
- Automatic Verification of the Adequacy of Models for Families of Geometric Objects
- Introduction
- An Outline of Our Method
- A Formal Description of Our Method
- Complexity
- Example Computations for Geometric Primitives
- Lines and Spheres in 2-Space
- Planes and Spheres in 3-Space
- Tori
- Circle Rings in 2-Space
- Tori in 3-Space
- Conclusions
- References
- Formalizing Projective Plane Geometry in Coq
- Introduction
- Axioms
- A First Set of Axioms
- Another Axiom System for Projective Plane Geometry
- Implementation in Coq
- Duality
- Principle of Duality
- Applications
- Models
- Finite Models
- Infinite Model: Homogeneous Coordinates
- Desarguesian and Non-desarguesian Models
- Desargues' Property
- Fano's Plane Is Desarguesian
- Independence of Desargues' Property
- Conclusion and Future Work
- References
- Linear Programming for Bernstein Based Solvers
- Introduction
- Tensorial Bernstein Bases, Definitions, Main Properties
- Definition of the Bernstein Polytope
- Univariate Polynomials
- Multivariate Polynomials
- Linear Programming
- Range Bound for a Polynomial
- Domain Reduction
- Use in Interval Newton Solvers
- New Solver
- Technicalities
- Scaling
- Inaccuracy Issues
- Guarantees and Theorems
- Solver Implementation
- Conclusion and Future Work
- References
- Offsetting Revolution Surfaces
- Introduction
- Surfaces of Revolution
- Implicitization of Revolution Surfaces
- Offsets to Revolution Surfaces
- References
- An Introduction to Java Geometry Expert
- Introduction
- The Parts of JGEX
- The Manual Input Method
- The Automated Methods
- Visualization of Fixpoints
- Conclusion
- References
- On the Heilbronn Optimal Configuration of Seven Points in the Square
- Introduction
- Reducing the Optimal Configuration to 226 Local Optimizations
- Checking the Loose Constraints of Non-linear Programming Problems
- Solving Non-linear Programming With Symbolic Computation
- Open Problems Related to the Heilbronn Configuration of Eight Points in the Square
- Conclusion
- References
- Author Index
