CSE Colloquium Series

ProofBuilder, a Pedagogically Oriented Prover

Dr. Hugh McGuire

School of Computing & Information Systems
Grand Valley State University

Tuesday, January 15, 2008
Talk: 11:00 am - 12:00 pm
3105 Engineering

Host: Laura Dillon

Abstract

This talk will present an interactive first-order theorem-proving system named ProofBuilder, which is pedagogically oriented. As with other systems, ProofBuilder covers a wide range of formal reasoning, from propositional simplification to strong induction; but what distinguishes ProofBuilder is that it is designed to enable users to prove theorems as much as possible like the way they do manually. Such aspects of the design include a framework that clarifies which formulas in a proof are premises that are hypothesized to be true, and which are goal formulas that need to be proven; and mechanisms to apply a variety of proof methods and strategies such as forward and backward reasoning, proving by contradiction, and proving by cases. ProofBuilder is intentionally interactive --- not completely automated --- also for pedagogical reasons: automated systems enable students to avoid the intellectual deductive work of doing proofs. But ProofBuilder does help students by: (i) structuring the proof and its construction clearly, avoiding confusion; (ii) showing in menus the variety of options for deduction such as simple rewriting, substituting using equations, and applying stepwise or strong induction; (iii) doing the work of performing menial symbolic manipulations, e.g. substituting ``0'' and ``n+1'' where appropriate when applying stepwise induction; and (iv) enforcing soundness of deductive steps.

ProofBuilder is written in Java, so it is usable on essentially all common modern platforms (Microsoft Windows, LINUX, Apple Macintosh, UNIX, etc.); and it has a graphical user interface, including capabilities for copying and pasting formulas from other convenient sources such as Web pages.

Biography

Hugh McGuire is an Assistant Professor of Computer Science at G.V.S.U. During Summer 2007, he is co-teaching CS 361, "System Programming (C and UNIX/LINUX)" . During Winter 2007, he taught CS 163, "Computer Science II", and MTH 225, "Discrete Structures: Computer Science 1" .

Previously, Hugh McGuire was a Lecturer, i.e. an instructor, in the Department of Computer Science at the University of California at Santa Barbara (U.C.S.B.). For a couple of years, in connection with the position of Lecturer, Hugh McGuire served as Undergraduate Academic Advisor .

Prior to that, Hugh McGuire was a Postgraduate Researcher for Professor Laura Dillon at U.C.S.B., researching specification and validation of concurrent software-systems, using graphical interval temporal logic.

In June, 1995, Hugh McGuire completed his doctoral studies in Computer Science at Stanford University, earning a Ph.D. with Distinction in Teaching . He taught several courses, including "Concurrent Programming" and "Unix Systems-Programming and C", and he also worked as a teaching-assistant for many courses. The subject of his dissertation was Temporal Logic, applicable to verification of concurrent systems, but Cognitive Science (involving 'Artificial Intelligence') also interests him. In 1985 he earned his A.B. cum laude from Harvard College, where he concentrated in Mathematics. In 1982, he transferred to Harvard from Deep Springs College . (Deep Springs is a two-dozen-student two-year liberal arts college whose campus is also a ranch. Students participate in the ranch-work and college-administration --e.g. one student is a member of the board of trustees -- while they do normal college courses. Click here for more material such as pictures of Deep Springs. )

Hugh has been a member of The Mathematical Association of America since he was 17, and he is a member of the Association for Computing Machinery (with specialized membership in SIGCSE , the Special Interest Group on Computer Science Education).

Hugh spent one year during high school as an exchange-student in France, where he became fluent in French.


Curriculum Vitae