| Machine verification of formal arguments increases our confidence in their correctness, but the costs of employing machine verification still outweigh the benefits for some common kinds of formal reasoning activity. Consequently, usability is becoming an important issue in the design of formal verification tools. We describe our development of the AARTIFACT lightweight verification system, which is designed for processing formal arguments involving basic, ubiquitous mathematical concepts. It integrates a variety of features and techniques, found in the literature on formal verification and other topics, that contribute to the system's overall usability. These include features that relate to syntax, user interface design, logical validation and inference, and ontology maintenance and management.The AARTIFACT system incorporates an expert-managed database of syntactic idioms, definitions, and propositions involving common mathematical concepts such as numbers, sets, vectors, and associated operators, relations, and predicates. A basic validation procedure for formal arguments utilizes common logical inference rules in conjunction with this database. This is accomplished by augmenting the data structure representing the context of bound variables and valid expressions with a component for computing congruence closures of expressions introduced by users. This validation procedure allows the system to meet user expectations by detecting implicit invocations of formal definitions and propositions, and by comprehending syntactic idioms employed by users.The system's interface allows users to author arguments using a conventional and flexible concrete syntax that supports user-defined predicates and operators, provides an interactive real-time lookup mechanism that reveals the supported syntactic constructs and database contents to users, and lets users select which validation procedure or logical system to employ. These features actively help users understand the system's capabilities and limitations within the context of the argument being authored, and help users better exploit the tradeoff between their confidence in an argument's validity and the effort required to have it certified as valid.The system's usability and performance are evaluated by examining use cases. These include employment of the system by instructors and students in a classroom setting, and the system's application in novel research efforts that require formal rigor. |
