Foreword
Preface
Contributors
1 Overview and Preliminaries
Meera Sitharam and Troy Baker
1.1 Introduction
1.1.1 Specifying a GCS
1.1.2 Fundamental GCS Questions
1.1.3 Tractability and Computational Complexity
1.2 Parts and Chapters of the Handbook
1.2.1 Part I��Geometric Reasoning Techniques
1.2.2 Part II��Distance Geometry��Configuration Space��and Real Algebraic Ge-ometry Techniques
1.2.3 Part III��Geometric Rigidity Techniques
1.2.4 Part IV��Combinatorial Rigidity Techniques
1.2.4.1 Inductive Constructions
1.2.4.2 Body Frameworks
1.2.4.3 Body-Cad��and Point-Line Frameworks
1.2.4.4 Symmetric and Periodic Frameworks and Frameworks under Polyhedral Norms
1.2.5 Missing Topics and Chapters
1.3 Terminology Reconciliation and Basic Concepts
1.3.1 Constrainedness
1.3.2 Rigidity of Frameworks
1.3.3 Generic Rigidity of Frameworks
1.3.4 Approximate Degree-of-Freedom and Sparsity
1.4 Alternative Pathway through the Book
I Geometric Reasoning��Factorization and Decomposition
2 Computer-Assisted Theorem Proving in Synthetic Geometry Julien Narboux��Predrag Jani?i?��and Jacques Fleuriot
2.1 Introduction
2.2 Automated Theorem Proving
2.2.1 Foundations
2.2.2 Nondegenerate Conditions
2.2.3 Purely Synthetic Methods
2.2.3.1 Early Systems
2.2.3.2 Deductive Database Method��GRAMY��and iGeoTutor
2.2.3.3 Logic-Based Approaches
2.2.4 Semisynthetic Methods
2.2.4.1 Area Method
2.2.4.2 Full-Angle Method
2.2.4.3 Vector-Based Method
2.2.4.4 Mass-Point Method
2.2.5 Prover s Implementations and Repositories of Theorems
2.3 Interactive Theorem Proving
2.3.1 Formalization of Foundations of Geometry
2.3.1.1 Hilbert's Geometry
2.3.1.2 Tarski’s Geometry
2.3.1.3 Axiom Systems and Continuity Properties
2.3.1.4 Other Axiom Systems and Geometries
2.3.1.5 Meta-Theory
2.3.2 Higher Level Results
2.3.3 Other Formalizations Related to Geometry
2.3.4 Verified Automated Reasoning
3 Coordinate-Free Theorem Proving in Incidence Geometry
Jürgen Richter-Gebert and Hongbo Li
3.1 Incidence Geometry
3.1.1 Incidence Geometry in the Plan e
3.1.2 Other Primitive Operations
3.1.3 Projective Invariance
3.2 Bracket Algebra��Straightening��Division��and Final Polynomials
3.2.1 Bracket Algebra and Straightening
3.2.2 Division
3.2.3 Final Polynomials
3.3 Cayley Expansion and Factorization
3.3.1 Cayley Expansion
3.3.2 Cayley Factorization
3.3.3 Cayley Expansion and Factorization in Geometric Theorem Proving
3.3.4 Rational Invariants and Antisymmetrization
3.4 Bracket Algebra for Euclidean Geometry
3.4.1 The Points I and J
3.4.2 Proving Euclidean Theorems
4 Special Positions of Frameworks and the Grassmann-Cayley Algebra
Jessica Sidman and William Traves
4.1 Introduction��the Grassmann-Cayley Algebra and Frameworks
4.2 Projective Space
4.2.1 Motivation
4.2.2 Homogeneous Coordinates and Points at Infinity
4.2.3 Equations on Projective Space
4.2.4 Duality Between Lines and Points in IP2
4.2.5 Grassmannians and Plücker Coordinates
4.2.6 More About Lines in 3-space
4.3 The Bracket Algebra and Rings of Invariants
4.3.1 Group Actions and Invariant Polynomials
4.3.2 Relations Among the Brackets
4.4 The Grassmann-Cayley Algebra
……
II Distance Geometry, Real Algebraic Geometry, and Configuration Spaces
III Geometric Rigidty
IV Combinatorial Rigidity