Recent work in constructive mathematics shows that Hilbert's program works for a large part of abstract algebra. Using in an essential way the ideas contained in the classical arguments, we can transform most of the highly abstract proofs of ‘concrete’ statements into elementary proofs. Surprisingly, the arguments we produce are not only elementary but also mathematically clearer, and not necessarily longer. We present an example where the simplification was significant enough to suggest an improved version of a classical theorem. For this we use a general method to transform some logically complex first-order formulae into a geometrical form, which may be interesting in itself.

Article Sturm-Habicht sequence Share on Authors: L. Gonzalez View Profile , H. Lombardi View Profile , T. Recio View Profile , M.-F. Roy View Profile Authors Info & Claims ISSAC '89: Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computationJuly 1989 Pages 136–146https://doi.org/10.1145/74540.74558Published:17 July 1989 36citation499DownloadsMetricsTotal Citations36Total Downloads499Last 12 Months11Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access