Accession Number : ADA130720

Title :   A Fully Automatic Proof of an Ordered Tree Insertion Function.

Descriptive Note : Technical rept.,

Corporate Author : TEXAS UNIV AT AUSTIN INST FOR COMPUTING SCIENCE AND COMPUTER APPLICATIONS

Personal Author(s) : Boyer,Robert S ; Moore,J Strother

PDF Url : ADA130720

Report Date : May 1983

Pagination or Media Count : 51

Abstract : The authors define the concept of an ordered binary tree, the concept that a number occurs in such a tree, and a function that is purported to insert a number into such a tree. They then show a fully automatic proof that the insertion function is correct. The machine proves the following three theorems without any help whatsoever. First, the recursive equation describing the insertion function is satisfied by one and only one function - in particular, the machine proves that the recursion always terminates. Second, if X is an ordered tree and L is a number, then the result of inserting L into X is an ordered tree. Third, if X is an ordered tree and L and K are numbers, then L occurs in the result of inserting K into X if and only if either L=K or L already occurred in X. (Author)

Descriptors :   *Topology, *Binary arithmetic, *Inserts, *Computers, Algorithms, Theorems, Recursive functions, Equations, Output

Subject Categories : Theoretical Mathematics
      Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE