Abstract
Here we give an automated proof of the fact that a cubic curve admits at most one group law. This is achieved by proving the tight connection between the chord-tangent law of composition and any potential group law (as a morphism) on the curve. An automated proof of this is accomplished by implementing the rigidity lemma and the Cayley-Bacharach theorem of algebraic geometry as formal inference rules in Prover9, a first-order theorem prover developed by Dr. William McCune.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Knapp, A.: Elliptic Curves. Princeton University Press (1992)
McCune, W.: Otter 3.0 Reference Manual and Guide. Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL (1994), http://www.mcs.anl.gov/AR/otter/
McCune, W.: Prover9, version 2009-02A, http://www.cs.unm.edu/~mccune/prover9/
Mumford, D.: Abelian varieties. Tata Institute of Fundamental Research. Studies in Mathematics, vol. 5. Oxford University Press, London (1970)
Padmanabhan, R.: Logic of equality in geometry. Discrete Mathematics 15, 319–331 (1982)
Padmanabhan, R., McCune, W.: Automated reasoning about cubic curves. Computers and Mathematics with Applications 29(2), 17–26 (1995)
Padmanabhan, R., McCune, W.: Uniqueness of Steiner laws on cubic curves. Beiträge Algebra Geom. 47(2), 543–557 (2006)
Padmanabhan, R., Veroff, R.: A geometric procedure with Prover9 (Web support) (2012), http://www.cs.unm.edu/~veroff/gL_Paper/
Padmanabhan, R., Veroff, R.: A gL clause generator (2012), http://www.cs.unm.edu/~veroff/gL_Paper/gL_gen.html
Silverman, J., Tate, J.: Rational Points on Elliptic Curves. Springer (1992)
Veroff, R.: Solving open questions and other challenge problems using proof sketches. J. Automated Reasoning 27, 157–174 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Padmanabhan, R., Veroff, R. (2013). A Geometric Procedure with Prover9. In: Bonacina, M.P., Stickel, M.E. (eds) Automated Reasoning and Mathematics. Lecture Notes in Computer Science(), vol 7788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36675-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-36675-8_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36674-1
Online ISBN: 978-3-642-36675-8
eBook Packages: Computer ScienceComputer Science (R0)