avg @ cs.ucsc.edu Office: E2-355 (831)459-4611	ALLEN VAN GELDER Professor of Computer Science Education: B.S., Mathematics, Massachusetts Institute of Technology Ph.D., Computer Science, Stanford University
Allen Van Gelder's research interests include development of algorithms for propositional satisfiability, methods for verifiable software, theorem proving, analysis of algorithms, parallel algorithms, computer graphics, and scientific visualization. He received a National Science Foundation Presidential Young Investigator Award in 1989 to investigate the use of logic programming for problems in database and artificial intelligence systems. Papers by Allen Van Gelder Various software ProofChecker documentation and code purse-poster.pdf SAT 2005 and 2007 Competition Scoring Rules purse-poster.ps       and some 2005 results Printable ISAIM 2008 Schedule isaim08-printable-sched.html isaim08-printable-sched.ps CMPS217, Logic in Computer Science, Fall 2007: Fall 2007 web page

SAT 2007 Lisboa/Lisbon Map (jpg)

Information on Winter 2007 CMPS 101

Office Hours, Winter 2007: MW 5:00-6:00, plus drop-in or appt.

c-adt.ps c-adt.pdf

For information about Computer Algorithms, Third Edition by Sara Baase and myself, please click here to see Supplements (including errata, clarifications, sample code, javaToC hints)
or shift-click to download Supplements.tar (about 320 KB)
or visit these links to other servers, and use the Back button on your browser if you want to return to this page.
Prof. Baase's web site: http://www-rohan.sdsu.edu/faculty/baase
AWL Publisher's information
Prof. Ben Choi's web site at Louisiana Tech University for PowerPoint slides to accompany the text. He offered to make them available to other instructors.
http://www2.latech.edu/~choi/Bens/Teaching/Csc520/

Please click here to see TPTPparser (lex/yacc sources, linux/intel binary, sample input, README, tarball)

Please click here to see http://jsat.ewi.tudelft.nl (Journal of Satisfiability home page)

ssh-cookbook Text file, what to do at soe to use ssh from outside soe. NOT KEPT UP.

Information on dbx for C programs on Solaris machines
Undergrads not in my course are welcome to use these files, but please consult your course's TAs and tutors with questions. Sorry, but there are hundreds of you.
Grads, instructors, visitors, I'll try to answer questions.

student-dbx-guide Text file, basics of using dbx. See CASE 3 for why to use cc/dbx rather than gcc/gdb.
student.dbxrc Sample dbx startup file, text, hopefully self-explanatory.

WhyIavoidGcc Judge for yourself.

Please click here to see Poster directory with some examples of using latex to make a poster.

My Erdös number is 3, e.g. through the path AVG - Jeff Ullman - Ron Graham - PE. Also, my Erdös number of the second kind (where only two-authored papers count) is ???, through the path AVG - ??? - PE. Thanks to Jan Johannsen for publicizing how to figure this out. Don't miss other interesting stuff on his home page, such as the Proof Complexity Theme Song.