Skip to main content
SpringerLink
Log in

Algebraic Representation, Elimination and Expansion in Automated Geometric Theorem Proving

  • Conference paper
Automated Deduction in Geometry (ADG 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2930))

Included in the following conference series:

Abstract

Cayley algebra and bracket algebra are important approaches to invariant computing in projective and affine geometries, but there are some difficulties in doing algebraic computation. In this paper we show how the principle “breefs” – bracket-oriented representation, elimination and expansion for factored and shortest results, can significantly simplify algebraic computations. We present several typical examples on automated theorem proving in conics and make detailed discussions on the procedure of applying the principle to automated geometric theorem proving.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barnabei, M., Brini, A., Rota, G.-C.: On the Exterior Calculus of Invariant Theory. J. Algebra 96, 120–160 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  2. Bix, R.: Conics and Cubics. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  3. Bokowski, J., Sturmfels, B.: Computational Synthetic Geometry. LNM, vol. 1355. Springer, Heidelberg (1989)

    Google Scholar 

  4. Chou, S.C.: Mechanical Geometry Theorem Proving. D. Reidel, Dordrecht (1988)

    MATH  Google Scholar 

  5. Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry—Automated Production of Readable Proofs for Geometric Theorems. World Scientific, Singapore (1994)

    Google Scholar 

  6. Crapo, H., Richter-Gebert, J.: Automatic Proving of Geometric Theorems. In: White, N. (ed.) Invariant Methods in Discrete and Computational Geometry, pp. 107–139. Kluwer Academic Publishers, Dordrecht (1994)

    Google Scholar 

  7. Doubilet, P., Rota, G.C., Stein, J.: On the Foundations of Combinatorial Theory IX: Combinatorial Methods in Invariant Theory. Stud. Appl. Math. 57, 185–216 (1974)

    MathSciNet  Google Scholar 

  8. Gao, X.S., Wang, D.: Mathematics Mechanization and Applications. Academic Press, London (2000)

    MATH  Google Scholar 

  9. Li, H., Wu, Y.: Automated Theorem Proving with Bracket Algebra in Projective Geometry. In: Gao, X.S., Wang, D. (eds.) Computer Mathematics, pp. 120–129. World Scientific, Singapore (2000)

    Google Scholar 

  10. Li, H., Wu, Y.: Automated Short Proof Generation for Projective Geometric Theorems with Cayley and Bracket Algebras, I. Incidence Geometry. J. of Symbolic Computation (to appear)

    Google Scholar 

  11. Li, H., Wu, Y.: Automated Short Proof Generation for Projective Geometric Theorems with Cayley and Bracket Algebras, II. Conic Geometry. J. of Symbolic Computation (to appear)

    Google Scholar 

  12. Li, H., Wu, Y.: Automated Theorem Proving in Affine Geometry with Cayley and Bracket Algebras (preprint)

    Google Scholar 

  13. Mourrain, B.: New Aspects of Geometrical Calculus with Invariants. Advances in Mathematics, Also in MEGA 1991 (1991) (to appear)

    Google Scholar 

  14. Richter-Gebert, J.: Mechanical Theorem Proving in Projective Geometry. Annals of Math. and Artificial Intelligence 13, 159–171 (1995)

    MathSciNet  Google Scholar 

  15. Richter-Gebert, J.: Realization Spaces of Polytopes. LNM, vol. 1643. Springer, Berlin (1996)

    Google Scholar 

  16. Sturmfels, B.: Computational Algebraic Geometry of Projective Configurations. J. Symbolic Computation 11, 595–618 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  17. Sturmfels, B.: Algorithms in Invariant Theory. Springer, New York (1993)

    MATH  Google Scholar 

  18. Sturmfels, B., Whiteley, W.: On the Synthetic Factorization of Homogeneous Invariants. J. Symbolic Computation 11, 439–454 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  19. Wang, D.: Elimination Methods. Springer, New York (2001)

    MATH  Google Scholar 

  20. White, N.: The Bracket Ring of Combinatorial Geometry I. Trans. Amer. Math. Soc. 202, 79–103 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  21. White, N.: Multilinear Cayley Factorization. J. Symb. Comput. 11, 421–438 (1991)

    Article  MATH  Google Scholar 

  22. McMillan, T., White, N.: The Dotted Straightening Algorithm. J. Symb. Comput. 11, 471–482 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  23. Whiteley, W.: Invariant Computations for Analytic Projective Geometry. J. Symb. Comput. 11, 549–578 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  24. Wu, W.T.: Mathematics Mechanization. Science Press/Kluwer Academic, Beijing (2000)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Mathematics Mechanization Key Lab Academy of Mathematics and System Sciences, Chinese Academy of Sciences, Beijing, 100080, China

    Hongbo Li

Authors
  1. Hongbo Li
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Research Institute for Symbolic Computation (RISC), J. Kepler University, Altenbergerstr. 69, A-4040, Linz, Austria

    Franz Winkler

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Li, H. (2004). Algebraic Representation, Elimination and Expansion in Automated Geometric Theorem Proving. In: Winkler, F. (eds) Automated Deduction in Geometry. ADG 2002. Lecture Notes in Computer Science(), vol 2930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24616-9_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24616-9_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20927-0

  • Online ISBN: 978-3-540-24616-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation