NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Press Enter or click the Search button to begin your search.

Back to Results
Using Decision Procedures to Build Domain-Specific Deductive Synthesis SystemsThis paper describes a class of decision procedures that we have found useful for efficient, domain-specific deductive synthesis. These procedures are called closure-based ground literal satisfiability procedures. We argue that this is a large and interesting class of procedures and show how to interface these procedures to a theorem prover for efficient deductive synthesis. Finally, we describe some results we have observed from our implementation. Amphion/NAIF is a domain-specific, high-assurance software synthesis system. It takes an abstract specification of a problem in solar system mechanics, such as 'when will a signal sent from the Cassini spacecraft to Earth be blocked by the planet Saturn?', and automatically synthesizes a FORTRAN program to solve it.
Document ID
20020061258
Acquisition Source
Ames Research Center
Document Type
Preprint (Draft being sent to journal)
Authors
VanBaalen, Jeffrey
(NASA Ames Research Center Moffett Field, CA United States)
Roach, Steven
(NASA Ames Research Center Moffett Field, CA United States)
Lau, Sonie
Date Acquired
September 7, 2013
Publication Date
January 1, 1998
Subject Category
Cybernetics, Artificial Intelligence And Robotics
Meeting Information
Meeting: 8th International Workshop on Logic-Based Program Synthesis and Transformation
Location: Manchester
Country: United Kingdom
Start Date: June 15, 1998
End Date: June 19, 1998
Funding Number(s)
PROJECT: RTOP 632-30-00
CONTRACT_GRANT: NAS2-14217
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
No Preview Available