ITR/SY: Computational Logic Tools for Research and Education

ITR/SY：用于研究和教育的计算逻辑工具

• 批准号: 0121403
• 负责人: David Dill
• 金额: --
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-10-01 至 2008-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0121403&HistoricalAwards=false
• 关键词: ITR; SY; Computational; Logic; Tools

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.

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