Accession Number:

ADA123268

Title:

Special Relations in Program-Synthetic Deduction,

Descriptive Note:

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1982-03-01

Pagination or Media Count:

77.0

Abstract:

Program synthesis is the automated derivation of a computer program from a given specification. In the deductive approach, the synthesis of a program is regarded as a theorem-proving problem the desired program is constructed as a by-product of the proof. This paper presents a formal deduction system for program synthesis, with special features for handling equality, the equivalence connective, and ordering relations. In proving theorems involving the equivalence connective, it is awkward to remove all the quantifiers before attempting the proof. The system therefore deals with partially skolemized sentences, in which some of the quantifiers may be left in place. A rule is provided for removing individual quantifiers when required after the proof is under way. The system is also nonclausal i.e., the theorem does not need to be put into conjunctive normal form. The equivalence, implication, and other connectives may be left intact. Author

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE