Abstract
Automated deduction techniques are being used in a system called Amphion to derive, from graphical specifications, programs composed from a subroutine library. The system has been applied to construct software for the planning and analysis of interplanetary missions. The library for that application is a collection of subroutines written in FORTRAN-77 at JPL to perform computations in solar-system kinematics. An application domain theory has been developed that describes the procedures in a portion of the library, as well as some basic properties of solar-system astronomy, in the form of first-order axioms.
Specifications are elicited from the user through a menu-driven graphical user interface; space scientists have found the graphical notation congenial. The specification is translated into a theorem, which is proved constructively in the astronomical domain theory by an automated theorem prover, SNARK. An applicative program is extracted from the proof and converted to FORTRAN-77. By the method of its construction, the program is guaranteed to meet the given specification and requires no further verification, provided, of course, that the specification, domain theory, and system itself are correct.
Amphion has successfully constructed more than a hundred programs to solve problems, formulated at NASA Ames, JPL, and Stanford, which involve typical computations involving the sun, planets, moons, and spacecraft. The system is currently being alpha tested at JPL.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. S. Boyer and J S. Moore, A Computational Logic Handbook, Academic Press, Boston, MA (1988).
N. Dershowitz, Orderings for Term-Rewriting Systems, Journal of Theoretical Computer Science, 17, 3 (1982), 279–301.
J. Hsiang and M. Rusinowitch, Proving Refutation Completeness of Theorem-Proving Strategies: The Transfinite Semantic Tree Method, Journal of the ACM, 38, 3 (1991), 559–587.
W. McCune, Otter 2.0 User's Guide, Technical Report ANL-90/9, Argonne National Laboratory, Argonne, IL (1990).
Z. Manna and R. Waldinger, Fundamentals of Deductive Program Synthesis, IEEE Transactions on Software Engineering, 18, 8 (1992), 674–704.
Z. Manna and R. Waldinger, Deductive Foundations of Computer Programming, Addison-Wesley, Reading, MA (1993).
J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12 (1965) 23–41.
E. J. Rollins and J. M. Wing, Specifications as Search Keys for Software Libraries, Eighth International Conference on Logic Programming, Paris, June 1991.
D. R. Smith, KIDS: A Semiautomatic Program Development System. IEEE Transactions on Software Engineering 16, 9 (1990) 1024–1043.
E. H. Tyugu, Knowledge-Based Programming, Turing Institute Press, Glasgow, Scotland, 1988.
L. Wos and G. Robinson, Paramodulation and Theorem Proving in First-Order Theories with Equality. In B. Meltzer and D. Michie (editors), Machine Intelligence 4, American Elsevier, New York, NY (1969) 135–150.
L. Wos, G. A. Robinson, and D. F. Carson, Efficiency and Completeness of the Set-of-Support Strategy in Theorem Proving. Journal of the ACM, 12, 4 (1965), 536–541.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stickel, M., Waldinger, R., Lowry, M., Pressburger, T., Underwood, I. (1994). Deductive composition of astronomical software from subroutine libraries. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_24
Download citation
DOI: https://doi.org/10.1007/3-540-58156-1_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58156-7
Online ISBN: 978-3-540-48467-7
eBook Packages: Springer Book Archive