• Skip to primary navigation
  • Skip to main content
SRI logo
  • About
    • Press room
    • Our history
  • Expertise
    • Advanced imaging systems
    • Artificial intelligence
    • Biomedical R&D services
    • Biomedical sciences
    • Computer vision
    • Cyber & formal methods
    • Education and learning
    • Innovation strategy and policy
    • National security
    • Ocean & space
    • Quantum
    • QED-C
    • Robotics, sensors & devices
    • Speech & natural language
    • Video test & measurement
  • Ventures
  • NSIC
  • Careers
  • Contact
  • 日本支社
Search
Close
Artificial intelligence publications June 1, 1994

The deductive composition of astronomical software from subroutine libraries

Citation

Copy to clipboard


Stickel, Mark and Waldinger, Richard and Lowry, Michael and Pressburger, Thomas and Underwood, Ian. The deductive composition of astronomical softwared from subroutine libraries, in Twelfth International Conference on Automated Deduction (CADE), Nancy, France, pp. 341-355, Jun 1994.

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.

↓ Review online

Share this

How can we help?

Once you hit send…

We’ll match your inquiry to the person who can best help you.

Expect a response within 48 hours.

Career call to action image

Make your own mark.

Search jobs

Our work

Case studies

Publications

Timeline of innovation

Areas of expertise

Institute

Leadership

Press room

Media inquiries

Compliance

Careers

Job listings

Contact

SRI Ventures

Our locations

Headquarters

333 Ravenswood Ave
Menlo Park, CA 94025 USA

+1 (650) 859-2000

Subscribe to our newsletter


日本支社
SRI International
  • Contact us
  • Privacy Policy
  • Cookies
  • DMCA
  • Copyright © 2022 SRI International