ITR/SY: Computational Logic Tools for Research and Education

形式逻辑是一种非常强大和通用的概念工具，如果可以通过计算来操纵它，它就会变得更加有用。由于计算逻辑通常难以实现且计算成本高，因此自动化的进展有些滞后。然而，这些问题及其解决方案正变得越来越容易理解，计算能力也在继续呈指数级增长，因此，为许多有趣的逻辑问题开发实用的计算解决方案的可能性现在是可以解决的。这个项目有三个主题：计算逻辑组件、教育应用和系统应用。第一个主题包括理论研究和实现工作，以开发用于在几个抽象层次上操作逻辑表示的实用软件组件，包括一阶逻辑片段的决策程序和一阶逻辑的自动演绎。第二个主题涉及在三个至关重要的应用领域中使用计算逻辑对设计进行计算机辅助分析：网络、混合系统和计算机安全。第三个主题是与计算机科学相关的数学概念教学课件的开发和在课堂上的使用。这项工作是与斯坦福大学的天才儿童教育计划（EPGY）合作进行的。这项工作的影响在于使计算逻辑变得可访问和可用。计算逻辑组件将使构建复杂的软件应用程序变得更容易，通过提供强大的现成构建块来解决否则无法处理的问题。改进的分析工具和技术将导致以更快的速度和更低的成本实现卓越的系统设计。教学软件将提高计算机科学专业学生的复杂程度和解决问题的能力。

Formal logic is an extremely powerful and general conceptual tool thatcan be made even more useful if it can be manipulated computationally.Since computational logic is often difficult to implement andcomputationally expensive, progress on automating it has laggedsomewhat. However, the problems and their solutions are becomingbetter understood and computational power has continued to advanceexponentially, so the possibility of developing practicalcomputational solutions to many interesting logic problems is nowpotentially solvable.There are three themes to the project: computational logic components,educational applications, and systems applications. The first themeencompasses both the theoretical research and implementation worknecessary to develop practical software components for manipulatinglogical representations at several levels of abstraction, includingdecision procedures for fragments of first order logic and automateddeduction for first-order logic. The second theme involves the use ofcomputational logic for computer-assisted analysis of designs in threeapplication areas of critical importance: networking, hybrid systems,and computer security. The third theme is the development and use inthe classroom of instructional courseware for mathematical conceptsrelevant to computer science. This work is in collaboration withStanford's Educational Program for Gifted Children (EPGY).The impact of this work follows from making computational logicaccessible and available. Computational logic components will make iteasier to construct sophisticated software applications, by providingpowerful off-the-shelf building blocks for solving problems that wouldnot otherwise be tractable. Improved analysis tools and techniqueswill result in superior system designs achieved faster and at lowercost. Instructional software will enhance the sophistication andproblem-solving abilities of computer science students.