Accessible Integrated Formal Reasoning Environments in Classroom Instruction of Mathematics

Presented as part of the 2012 HCSS conference.

Abstract:

Computer science researchers in the programming languages and formal verification communities, among others, have produced a variety of automated assistance and verification tools and techniques for formal reasoning: parsers, evaluators, proof-authoring systems, software and hardware. These leading-edge advances remain largely underutilized by large populations of potential users that may benefit from them. Among these are instructors and students engaged in the undergraduate-level instruction and study of mathematics.

Tools such as MATLAB and Mathematica are utilized for solving problems by both instructors and students in mathematics courses at the undergraduate level. Other existing tools such as Isabelle/Isar [12], Mizar [11], Coq, or even basic techniques such as monomorphic type checking, computation of congruence closures, and automated logical inference, provide an unambiguous way to represent and verify formal arguments, from chains of basic algebraic manipulations in arithmetic all the way up to graduate-level mathematics topics. What impediments cause these tools to be so seldom used in presenting and assembling even basic algebraic arguments and proofs in undergraduate mathematics courses? Impediments faced by instructors and students who may wish to adopt existing automated formal reasoning assistance and verification tools and techniques include (we cite examples of related work that shares our motivation in addressing each impediment listed): syntaxes that may be unfamiliar and entirely distinct from the syntax used in textbooks and lecture materials [7]; a lack of high-level domain-specific libraries that would make formal arguments as manageable as those found in a text-book (or those presented in the classroom) [1, 3, 10]; a potentially idiosyncratic semantics focused on low-level logical correctness rather than practical high-level relationships typically explored in a mathematics course; a steep learning curve in employing a tool or technique [2, 5]; and logistical difficulties in setting up a working environment letting instructors and students use the same tools without much supporting IT infrastructure [5, 6].

Building on earlier work in assembling and evaluating user-friendly and accessible formal verification tools for research and classroom instruction [4, 8, 9], we have recently attempted to address many of these issues while making more manageable the task of utilizing existing formal reasoning assistance and verification techniques within the classroom. We have assembled a web-based integrated formal reasoning environment for classroom instruction that incorporates several standard techniques drawn from work done by the programming languages and formal verification communities over the last several decades. These techniques include basic evaluation of expressions, monomorphic type inference, basic verification of a subset of logical formulas in propositional and first-order logic, and an algorithm for computing congruence closures. This interactive web-based environment can run entirely within a standard web browser, and can be seamlessly integrated with a web page of lecture materials and homework assignments. The lectures and assignments contain within them formal arguments (including both complete examples and problems to be completed) that can be evaluated and/or automatically verified interactively. The environment provides an explicit library of logical definitions and formulas that students can utilize to complete assignments; these formulas can be browsed and filtered by students within the environment. The environment provides interactive and instant verification feedback about logical validity as well as an interactive, exhaustive list of all inferred properties for a given formal argument input.

The environment has been utilized within the classroom for an undergraduate-level course in linear algebra, both by the instructor in presenting examples during lectures, and by students when completing homework assignments. The focus of this work is not on the expressiveness or performance of the underlying tools and techniques within the environment (most examples used in such a course are simple); rather, it is on the design and practical evaluation of an integrated environment of basic, existing tools and techniques that is accessible (logistically and semantically) to non-expert end-users. We found that even basic capabilities are helpful in teaching students what is a formal argument and how to assemble a formal argument by examining possible formulas and applying those formulas while working towards a goal. Students were also able to transfer to an exam setting the techniques they used in assembling formal arguments within the environment.

Biography:

Andrei Lapets is a postdoctoral fellow at the Hariri Institute at Boston University. His research interests lie in finding ways to improve and measure the usability and accessibility of formal reasoning assistance tools and techniques. In 2011 he received a Ph.D. in Computer Science from Boston University, and he also holds S.M. and A.B. degrees in Computer Science and Mathematics from Harvard University.

References:

[1] A. Abel, B. Chang, and F. Pfenning. Human-Readable Machine Verifiable-Proofs for Teaching Constructive Logic. In U. Egly, A. Fiedler, H. Horacek, and S. Schmitt, editors, PTP ’01: IJCAR Workshop on Proof Transformations, Proof Presentations and Complexity of Proofs, Siena, Italty, 2001.

[2] A. Asperti, C.S. Coen, E. Tassi, and S. Zacchiroli. User Interaction with the Matita Proof Assistant. Journal of Automated Reasoning, 39(2): 109-139, 2007.

[3] C.E. Brown. Verifying and Invalidating Textbook Proofs Using Scunak. In MKM ’06: Mathematical Knowledge Management, pages 110-123, Wokingham, England, 2006.

[4] V. Ishakian, A. Lapets, A. Bestavros, and A. Kfoury. Formal Verification of SLA Tranformations. In Proceedings of CloudPerf 2011:IEEE International Workshop on Performance Aspects of Cloud and Service Virtualization, Washington, D.C., USA, July 2011.

[5] D. Jackson. Alloy: A Lightweight Object Modeling Notation. Software Engineering and Methodology, 11(2):256-290, 2002.

[6] C. Kaliszyk. Web Interfaces for Proof Assistants. Electronic Notes in Theoretical Computer Science, 174(2):49-61, 2007.

[7] F.Kamareddine and J.B. Wells. Computerizing Mathematical Text with MathLang. Electronic Notes in Theoretical Computer Science, 205:5-30, 2008.

[8] A. Lapets. User-Friendly Support for Common Concepts in a Lightweight Verifier. In Proceedings of VERIFY-2010: The 6th International Verification Workshop, Edinburgh, UK, July 2012

[9] A. Lapets and A. Kfoury. A User-friendly Interface for a Lightweight Verification System. In Proceedings of UITP’10: 9th International Workshop on User Interfaces for Theorem Provers, Edinburgh, UK, July 2010.

[10] J.H. Siekmann, C. Benzmuller, A. Fiedler, A. Meier, and M. Pollet. Proof Development with OMEGA: sqrt(2) Is Irrational. In LPAR, pages 367-387, 2002.

[11] A. Trybulex and H. Blair. Computer Assisted Reasoning with MIZAR. In Proceedings of the 9th IJCAI, pages 26-28, Los Angeles, CA, USA, 1985.

[12] M. Wenzel. The Isabelle/Isar Reference Manual, January 2011.