
Accession Number : ADA113431
Title : Derived Preconditions and Their Use in Program Synthesis.
Descriptive Note : Technical rept.,
Corporate Author : NAVAL POSTGRADUATE SCHOOL MONTEREY CA
Personal Author(s) : Smith,Douglas R
PDF Url : ADA113431
Report Date : Mar 1982
Pagination or Media Count : 31
Abstract : In this paper we pose and begin to explore a deductive problem more general than that of finding a proof that a given goal formula logically follows from a given set of hypotheses. The problem is most simply stated in the propositional calculus: given a goal A and hypothesis H we wish to find a formula P, called a precondition, such that A logically follows from both P and H. A precondition provides any additional conditions under which A can be shown to follow from H. A slightly more complex definition of preconditions in a firstorder theory is given and used throughout the paper. A formal system based on natural deduction is presented in which preconditions can be derived. A number of examples are then given which show how derived preconditions are used in a program synthesis method we are developing. These uses include theorem proving, formula simplification, simple code generation, the completion of partial specifications for a subalgorithm, and other tasks of a deductive nature. (Author)
Descriptors : *Goal programming, *Problem solving, Hypotheses, Mathematical logic, Theorems, Formulas(Mathematics), Coding, Specifications, Formulations, Simplification
Subject Categories : Theoretical Mathematics
Distribution Statement : APPROVED FOR PUBLIC RELEASE