SHF: Small: Little Tricky Logics: Misconceptions in Understanding Logics and Formal Properties

在计算机科学中，形式逻辑被广泛用于精确地陈述用户的意图。这些可以以许多不同的方式使用：可以检查现有系统以符合这些陈述，或者甚至可以生成遵循这些意图的新系统。然而，人类经常对这些逻辑有各种各样的误解，从而影响了它们的任何后续使用：如果逻辑陈述的意思与人类的意图不同，那么它不仅是无用的，而且是积极的误导。该项目的新颖之处在于阐明了这些误解，并评估了纠正这些误解的方法。该项目的影响包括帮助教育、创建帮助作者的工具，以及设计新的形式逻辑。具体而言，该项目旨在调查三种形式设置中的误解：线性时间逻辑，合金语言（具有传递闭包的一阶逻辑），以及在形式规范中广泛使用的基本结构属性（如传递性）。该项目使用多种方法来引出误解，同时考虑到克服专家盲点的需要。该项目还采用了现有的误解文献中的技术来克服它发现的问题。由此产生的解决误解的研究工具和技术将在许多情况下立即有用，并且工作的一般流程将广泛适用于希望根据其首选逻辑复制它的其他人。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Formal logics are widely employed in computer science to precisely state a user's intent. These can be used in many different ways: an existing system can be checked to conform to these statements, or a fresh system can even be generated that obeys these intentions. However, humans often have various misconceptions about these logics, which taints any subsequent use of them: if the logical statement means something other than what the human intends, then it is not merely useless, it is actively misleading. The project's novelties are to elucidate these misconceptions and to evaluate methods to correct them. The project's impacts are in aiding education, in the creation of tools to help authors, and also in the design of new formal logics.Concretely, the project aims to investigate misconceptions in three formal settings: Linear Temporal Logic, the Alloy language (a first-order logic with transitive closure), and in basic structural properties used widely in formal specification (such as transitivity). The project uses a variety of methods to elicit misconceptions, taking into account the need to overcome expert blind spots. The project also employs techniques from the existing misconception literature to overcome the problems that it finds. The resulting study instruments and techniques to address misconceptions would be immediately useful in many settings, and the general flow of the work would be broadly applicable to others who wish to reproduce it for their preferred logics.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.