ITR/SY: Computational Logic Tools for Research and Education

Stanford University, Stanford CA

Investigators

Abstract

Formal logic is an extremely powerful and general conceptual tool that can be made even more useful if it can be manipulated computationally. Since computational logic is often difficult to implement and computationally expensive, progress on automating it has lagged somewhat. However, the problems and their solutions are becoming better understood and computational power has continued to advance exponentially, so the possibility of developing practical computational solutions to many interesting logic problems is now potentially solvable. There are three themes to the project: computational logic components, educational applications, and systems applications. The first theme encompasses both the theoretical research and implementation work necessary to develop practical software components for manipulating logical representations at several levels of abstraction, including decision procedures for fragments of first order logic and automated deduction for first-order logic. The second theme involves the use of computational logic for computer-assisted analysis of designs in three application areas of critical importance: networking, hybrid systems, and computer security. The third theme is the development and use in the classroom of instructional courseware for mathematical concepts relevant to computer science. This work is in collaboration with Stanford's Educational Program for Gifted Children (EPGY). The impact of this work follows from making computational logic accessible and available. Computational logic components will make it easier to construct sophisticated software applications, by providing powerful off-the-shelf building blocks for solving problems that would not otherwise be tractable. Improved analysis tools and techniques will result in superior system designs achieved faster and at lower cost. Instructional software will enhance the sophistication and problem-solving abilities of computer science students.