| タイトル | Using Decision Procedures to Build Domain-Specific Deductive Synthesis Systems |
| 本文（外部サイト） | http://hdl.handle.net/2060/20020061258 |
| 著者（英） | Roach, Steven; Lau, Sonie; VanBaalen, Jeffrey |
| 著者所属（英） | NASA Ames Research Center |
| 発行日 | 1998-01-01 |
| 言語 | eng |
| 内容記述 | This 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. |
| NASA分類 | Cybernetics, Artificial Intelligence and Robotics |
| 権利 | No Copyright |
| URI | https://repository.exst.jaxa.jp/dspace/handle/a-is/91415 |
