Home page of Robert Stephen Boyer
Home mailing address:
614 W. 32nd St.
Austin, TX 78705
Publications
Graduated Ph. D. students
Honors
Employment
The Nqthm theorem prover, some examples of its use, and documentation of its
logic and user commands.
Links
- Bill McCune, and his
splendid provers
Otter/Mac2, and their successors Prover9/Mace4.
- Java Geometry
Expert Work by Chou, Gao, Zhang, Ye -- see the Butterfly, Morely, Pappus,
Pascal, Peaucellier, Simson and many more amazing geometry theorems proved in
a beautifully moving way. (http://woody.cs.wichita.edu/gex/index.html)
- Can machines think? Can you can prove the following easily stated
theorem, as did the program Otter? http://www.cs.unm.edu/~veroff/MEDIAN_ALGEBRA/.
-
The manuscripts of
E. W. Dijkstra, online Donald Knuth has remarked about Dijkstra that
"His uncompromising insistence on elegance in programming has always been an
inspiration to me (and doubtless to thousands of others)."
-
My ftp
directory Technical reports and Ph. D. theses, plus sources,
executables, and examples of use for several computer programs, mainly in the
research areas of program verification and automated reasoning. The exact
same material may be obtained at ftp://ftp.cs.utexas.edu/pub/boyer, which is
to say, via anonymous ftp to ftp.cs.utexas.edu, under directory pub/boyer.
About one gigabyte of material, authored by many people.
The whole 9 yards.
-
The QED project
-
More of Chou's geometry work.
Pythagoras would especially
love this dynamic page.
-
The Collected Works of Larry Wos An amazing collection of scientific papers in
automated reasoning. Blurbs.
- The Association for Automated Reasoning
Newsletter
- FM9001:
The verified microprocessor
Standard disclaimer
Nothing on my web pages should be taken as representing the official position
of the University of Texas at Austin or any other part of the government of
the State of Texas.
Two Photos of Me
2004
1991
