
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