A Fully Automatic Proof of an Ordered Tree Insertion Function.

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)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1983
Accession Number
ADA130720

Entities

People

  • J. Strother Moore
  • Robert S. Boyer

Organizations

  • University of Texas at Austin

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Arithmetic
  • Automatic
  • Computer Programming
  • Computer Science
  • Computers
  • Equations
  • Recursive Functions
  • Security
  • Trees (Data Structures)

Fields of Study

  • Mathematics

Readers

  • Graph Algorithms and Convex Optimization.