[net.ai] Automatic Deduction talk

TREITEL@SUMEX-AIM.ARPA (04/06/84)

From:  Richard Treitel <TREITEL@SUMEX-AIM.ARPA>

          [Forward from the Stanford bboard by Laws@SRI-AI.]

                Monday, April 9th in MJH 301 at 2:30.


                    THE ORIGIN OF BINARY-SEARCH ALGORITHMS


                               Richard Waldinger
                        Artificial Intelligence Center
                               SRI International


     Many of the most efficient numerical algorithms employ a binary search, in
which  the  number we are looking for belongs to an interval that is divided in
half at each iteration.  We consider how such algorithms might be derived  from
their specifications.

     We follow a deductive approach, in which programming is regarded as a kind
of  theorem  proving.    By  systematic  application  of this approach, several
integer and real-number algorithms for such functions as the  square  root  and
quotient have been derived.  Some of these derivations have been carried out on
an  interactive  program-synthesis  system.    The  programs  we  obtained  are
different from what we originally expected.