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

Brown University, Providence RI

Investigators

Abstract

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.