The Openproof Project at CSLI: Research


Current Members

Dave Barker-Plummer

Dave Barker-Plummer is an Senior Research Scientist at Stanford University's Center for the Study of Language and Information. He holds a Ph.D. from the Department of Artificial Intelligence at Edinburgh University. Since 1995 he has managed the Openproof project's work on educational software for teaching logic at the undergraduate level.  He is the author of papers on automated reasoning, reasoning with diagrams, and architectures for heterogeneous reasoning.  He co-edited the collection Words, Proofs and Diagrams and was program chair of the Diagrams 2006 conference. Dave has taught computer science and logic at Stanford, Swarthmore College and Duke University.

John Etchemendy is a professor of philosophy and symbolic systems at Stanford University.

Michael Murray is a Software Developer at CSLI.

Affiliated Members


Dr. Richard Cox is an Honorary Fellow in the School of Informatics at the University of Edinburgh, and a Visiting Senior Research Fellow in the Dept of Informatics, University of Sussex. He co-founded the Representation and Cognition Research Group at the University of Sussex.

Richard is extensively involved with the UK ESRC's Technology Enhanced Learning (TEL) Programme, serving as a member of the advisory board for the programme, the leader of the Technology Enhanced Research thematic strand, and as a member of the TEL programme's Impact Team.

His background is in psychology, education, and AI in education. He obtained his PhD in A.I. from the University of Edinburgh. Richard's research interests lie in the areas of cognitive education, human reasoning, diagrammatic reasoning, and individual differences. He has published over 30 journal papers and book chapters, and over 60 refereed conference papers in the areas of cognitive science, education, psychology and informatics.

Dr. Robert Dale is a Professor in the Department of Computing in the Division of Information and Communication Sciences at Macquarie University. His current research interests centre around intelligent text processing, natural language generation, and spoken language dialogue systems. He is also a member of the executive committee of the Association for Computational Linguistics, and a member of the Conference Co-ordinating Committee of the Asian Federation of Natural Language Processing. He writes a semi-regular column in the Journal of Natural Language Engineering called Industry Watch.

Robert Dale is author or editor of seven books and over 90 papers in various aspects of natural language processing. His current research interests include low-cost approaches to intelligent text processing tasks; practical natural language generation; the engineering of habitable spoken language dialog systems; and computational, philosophical and linguistic issues in reference and anaphora. He is editor of Computational Linguistics, the field's most prestigious journal, and has been Program Chair for conferences of both the Association for Computational Linguistics and the International Conference on Spoken Language Processing, the two premier events in the field; he was the Local Organising Committee Chair for the Coling/ACL 2006 conference, held in Sydney.

His motto is: leave things better than you found them.

Atsushi Shimojima is Professor of Culture and Information Science at Doshisha University in Japan. He received his doctoral degree from the Philosophy Department at Indiana University in 1996. His research so far has been focused on applying semantical analysis of diagrammatic systems to make predictions on their cognitive potentials and verifying these predictions on the basis of psychological experimentation. A good sample of this coupling of semantic analysis and cognitive science is found in his recent publication with Yasuhiro Katagiri in the journal, Cognitive Science, entitled "A Eye-Tracking Study of Exploitations of Spatial Constraints in Diagrammatic Reasoning.'' His work on the semantics of diagrams is being crystalized into a book, Semantic Properties of Diagrams and Their Cognitive Potentials, to be published in 2014. He is currently interested in formalizing his theory in the framework of channel theory (Barwise & Seligman 1997) to make it more readily applicable to real-world diagrammatic systems.

Dr. Nik Swoboda is currently a Ramón y Cajal Research Professor at the Universidad Politécnica de Madrid.  He received his undergraduate degree from Haverford College, and then completed a MS and Ph.D. in Computer Science at Indiana University.  His main research interest is in diagrammatic reasoning and the nature of non-sentential representation systems. He also collaborates in cognitive science research studying the use of graphical representations in communication. In his spare time he enjoys taking day hikes, traveling, and eating tasty Japanese and Spanish food.  He dreams of the day when he can forsake computers and spend his days sailing and fishing, but in the meantime, he utilizes his imagination to enjoy the world of sailing in sea adventure novels.

Past Members

Dr. Gerard Allwein is currently at the Naval Research Laboratory in Washingon, D.C., USA. His undergraduate is from Purdue University and holds graduate degrees from Indiana University. Upon graduation, he served as the Visual Inference Laboratory's Assistant Director under Jon Barwise. Dr. Allwein works primarily in mathematical aspects of logic and information. His current interests are defining relationships among mathematical modeling paradigms, diagrammatic reasoning, algebraic logic, and information hiding. His Siamese co-investigators are Tinkerbell and Ariel.

The late Jon Barwise was a professor of philosophy, mathematics, and computer science at Indiana University in Bloomington.

Anne Bracy worked at Openproof from 1996-1998, developing tools for diagrammatic reasoning with Venn diagrams. Later, she worked on a semantic grammar for a multi-modal dialogue system at the the Computational Semantics Laboratory, also at CSLI. At Stanford, Anne received a BA in German Studies, a BS in Symbolic Systems, and an MS in Computer Science. Anne then received a PhD in computer architecture from the University of Pennsylvania. After 4 years as a Research Scientist at Intel Labs in Santa Clara, CA, Anne moved to Missouri, where she teaches at Washington University in St. Louis.

Dr. Alan Bush is CEO of Sharefare Corporation.   Sharefare Corporation is creating a new kind of consumer oriented Internet service. Dr. Bush has been a management consultant at Bain & Company, Director of Products at software maker BEA Systems, engineering lead at Hewlett-Packard and Borland International, and a software entrepreneur.  He wrote his Ph.D. at Stanford University.  His main advisor was Prof. John Etchemendy.  His advisors included Prof. Jon Barwise, Prof. Johan van Benthem and Prof. John Perry.  His dissertation: "Media and Meaning: A Schematic Approach to Representational Semantics and its Applications" formalized a framework underlying the model-theoretic approach to modeling the consequence relation.  Dr. Bush used that framework to create alternative approaches, including two new techniques based on order and consistency, instead of truth and models.  He developed the initial specification for Hyperproof while an undergraduate at Stanford.

JT Chipman is a doctoral student in Stanford's Department of Philosophy, with his research focusing on mathematical logic, philosophy of logic, and the history of analytic philosophy. He also likes to think about logic pedagogy. JT spends his free time reading literature, watching movies, listening to music, and (with less frequency than he'd like) travelling.

Ben Davidson worked on the Openproof Project from 2002 to 2004 while an undergraduate at Stanford. He helped develop Tarski's World in Java and worked on the new edition of the TW text. His interests include personal identity, undergraduate education, and constitutional law. Ben now holds a B.S. in Symbolic Systems and works at Stanford's Undergraduate Research Programs office.


Brad Dolin was last seen on a Fulbright scholarship in Spain.

Matt Falkenhagen is currently a member of the Software Innovation Lab at Fujitsu Laboratories in Kawasaki, Japan. He received his B.S. and M.S. in Computer Science from Stanford University. He worked as a software developer on the Openproof Project in 2003-2004 while an undergraduate.


Rachel Farber was last seen working for Microsoft.

Mark Greaves currently serves as Program Manager for DARPA's UltraLog and DAML Projects.  He was previously Director of DARPA's Joint Logistics Technology Office and Program Manager for DARPA's Advanced Logistics Project.  At DARPA, Mark is responsible for pursuing aggressive development of advanced information technology that will cause a fundamental change in the way military planning and operations are conducted today. In particular, he is working on the application of autonomous agent technology to problems of information systems survivability and the control of complex systems-of-systems, and he leads DARPA's effort in the creation of logic languages for the Web (that is, Semantic Web technology).  Prior to coming to DARPA in 2001, Mark led advanced programs in software agent technology at the Mathematics and Computing Technology group of Boeing Phantom Works, the research division of the Boeing Co.


Albert Liu spent twelve years as a Senior Software Developer at CSLI.

Evan Liu is an undergraduate at Stanford University studying mathematics and computer science. The wide range of applications of logic - from writing analysis proofs to deciphering Kant to conversing with a friend - really excites me. My perspective of the world has entirely changed since studying logic. Besides logic, I like to spend my time playing tennis, studying chess, and baking.

Chris Newell is studying Philosophy as an undergraduate at Stanford University. He reads books and comics in his free time.

Emma Pease served as system administrator (and much more) for the Openproof project for five years.


Thomas S. Robertson graduated from Stanford in 2000 with a B.S. in Symbolic Systems.  He worked at HighWire Press for about a year and a half before switching to LOCKSS where he is currently the Assistant Director and Technical Manager.

Leslie Rogers worked with the Openproof project an undergraduate at Stanford University. She majored in Symbolic Systems with a concentration in Human Computer Interaction. Leslie was last seen working for Microsoft.

Su Su received her B.A. in Cognitive Psychology from Stanford University in June 2013, and a Masters in Instructional Technology & Media from Teachers College, Columbia University in 2015. Taking logic courses at Stanford was the best part of her undergraduate memories at Stanford. Her interests include logic and reasoning in education; using technology to spread logic around is the coolest thing she could ever think of!


Sara Tahir was last seen working for Microsoft.