Background, motivation, and discussion
From Automated Assistance for Formal Reasoning
We review the characteristics of the aartifact system's components (user interface, validation capabilities, and library) and cite related work (consisting of tools, discussion, or both) that motivates, describes, or develops these characteristics.
The user encodes formal arguments using a concrete syntax. There are three commonly recognized characteristics of a user-friendly concrete syntax.
- simple structure [9,10,11,12,17,18]
- no requirement for explicit annotations or references [9,10]
- familiar and consistent with prevailing conventions [9,10,11,18]
If a concrete syntax possesses a simple structure, it becomes necessary to reveal the practical syntax: the idioms a user must employ. It is necessary to support a large collection of conventional idioms, and to provide syntactic idioms for constructs for which there are no consistent prevailing conventions (as in the case of concrete syntax for vector concatenation, or definition of graphs). An interactive means for informing user of the latter is essential.
- large database of syntactic idioms
- passive interface for discovery (search) [22,23,24]
- active interface for discovery (real-time syntax lookup and hints [25,26,27], presentation of possible interpretations [23])
All the supported syntactic constructs have semantic interpretations. A large collection of definitions and propositions must be available to the user while authoring and verifying a formal argument. Furthermore, the user should have a large amount of control over the trade-off between certainty of validation and argument complexity/validation efficiency (in time and space).
- simple inference algorithm
- large database of definitions and propositions
- real-time data structure for validation without explicit reference (congruence closures [19,20,21], relevant work in SMT solvers)
- selection of logical system and validation procedure (trade-off between certainty and response time/argument complexity [1])
- implicit (feedback about what is sufficient, nested verification)
- explicit (specified through interface by user)
Integration with content management systems can aid in the expansion of libraries, in the assembly of results [8]. When coupled with cloud computing, such integration can aid in utilization of verification systems within communities and classrooms.
Contents |
Background
In research areas involving mathematical rigor, there are numerous benefits to adopting a formal representation of models, arguments, and results: verification of consistency and correctness, reusability, and automatic evaluation of instances and examples. However, to date, broad accessibility has not been a priority in the design of formal verification tools that can provide these benefits. Existing usability improvements are directed mostly towards researchers working with compilers, programming languages, and foundations of mathematics. In attempting to apply these tools to problems in their own area, researchers must laboriously translate existing concepts into a representation that does not retain the familiar conventions prevalent in their own community. This greatly reduces the perceived usefulness and increases the perceived difficulty of constructing and maintaining machine-verified models and proofs.
Traditional practices in computer science domains lying outside of programming language and compiler research suggest several requirements that the interface of an accessible tool should satisfy. The interface should permit natural language phrasing, familiar domain-specific syntax and symbols, the introduction (and utilization without explicit reference) of acceptable domain-specific symbolic manipulations, ``ambiguous" notation, and domain-directed choice of underlying logic(s). Our aim is to evaluate in practice whether existing lightweight verification techniques, combined with ad hoc domain-specific heuristics, can still provide the familiar benefits of formal verification while respecting these long-standing traditions. We do so by constructing a lightweight verification tool for proofs written in a mixture of English phrases and LaTeX syntax.
Motivating Assumptions
In undertaking the construction of a more friendly formal verification system, we make a few assumptions. We first assume that researchers are not willing to learn existing state-of-the-art systems. Currently, there exists a variety of tools for formal representation and machine verification of proofs. Some of these tools provide a way to construct proofs by induction, such as Coq, Isabelle, or PVS. Others allow the construction of static models using first order logic, such as Alloy. However, despite the existence of such tools for machine verification of proofs, researchers outside the programming language design community have largely chosen to ignore them. In the literature in other areas of computer science, there are only isolated attempts to include machine-verified proofs of research results.
Furthermore, we assume that this unwillingness is a result of an inadequate interface and a lack of concern about the user experience in a broader sense, and not a result of any fundamental limitation or inapplicability of formal verification. Existing systems are geared mostly towards researchers in languages and formal systems, and are thus inadequate for many other domains. Even though some tools allow interactive, goal-oriented proof construction, these interfaces do not reflect or acknowledge the proof writing process and conventions of researchers in other areas. As formal reasoning is ubiquitous in all areas of computer science research, we hypothesize that in at least some of these areas, researchers would indeed benefit from formal verification techniques. We can test this hypothesis only by providing a sufficiently accessible tool that can help researchers determine the extent to which it might be useful in their own area while minimizing the costs associated with doing so.
As developers, users, and proponents of formal verification techniques, we have incentives for exporting existing verification techniques to other domains. First, successful applications could demonstrate the applicability of existing verification techniques, thus providing invaluable publicity for the area of formal verification. Furthermore, by discovering limitations of existing techniques with input from other domains, we may find novel and interesting research opportunities in formal verification.
Representing and Documenting Common Logical and Symbolic Manipulations
When constructing and manipulating formal arguments, human authors employ a wide variety of symbolic transformations and shortcuts. To the best of our knowledge, there exists no system that has as one of its stated goals the extensive and thorough documentation of such techniques. Instead, users of existing tools are expected to adapt their style to the conventions and features available in the particular tool being employed. Such a library could be used to improve interfaces for verification systems. Furthermore, such a library could provide some insight into the kinds of strategies authors use when reasoning formally.
Related Work
MathLang
The MathLang project [2] is an extensive, long-term effort which aims to make natural language an input method for mathematical arguments and proofs. Natural language arguments are converted into a formal grammar (without committing to any particular semantics), and the participants are currently working on ways of converting this representation into a fully formalized logic. The MathLang project is focused primarily on mathematical texts, and representative texts from different areas are used as a guide in determining the direction of future research in the project.
From the perspective of a researcher, there are several drawbacks to using the MathLang project's system. A user wishing to take advantage of this system must use a specialized editor associated with the MathLang project. This approach does not leverage the existing knowledge of the research community: researchers already use certain kinds of tools to present their arguments, and forcing them to learn a new environment amounts to yet another disincentive. Furthermore, by choosing a formal semantics for the grammatical representation based on existing logic systems rather than the needs of researchers in a particular area, the project may inherit the disincentives associated with using existing machine verification systems. Also, the project makes no attempt to provide a friendly and familiar way to deal with the representation of algorithms, an essential component for computer science researchers. More generally, the project has a broad focus, and so the tools associated with it cannot easily cater to the needs of researchers in a particular area. In contrast, our work focuses on a prototype which is vertically integrated (from representation down to formal semantics), and for which every design decision is based entirely on providing the bare essentials necessary to meet the immediate needs of researchers presenting new proofs.
Integrated formal document verifier
In recent work [7], a proof verifier has been integrated with the scientific text editor TEXMACS. As in our work, the authors defined a concrete syntax that consists of selected English phrases and LaTeX syntax. Furthermore, the authors also advocate an interactive verification experience in which the verifier performs a search to ``fix" incomplete proofs. This differs from our view of search heuristics: we view them as an essential feature that ensures that a user need only write ``explicit results" in her proof, without specifying the law or rule being applied in deriving a particular result. We also advocate a more lightweight approach. We allow the user to choose to verify only parts of her document, and we do not restrict our system to any particular underlying logic. This is largely because our efforts are focused on providing an interface and supporting heuristics that scale well to larger proofs that involve many domain-specific facts and arguments. It is our belief that while this makes it more difficult to be completely certain in the validity of a proof even if it is verified, it still provides a proof author with valuable feedback and detection of many common errors.
``vdash"
A formal math wiki, ``vdash", [8] is currently being developed. Their current plan is to integrate the Isabelle [4] theorem prover with MediaWiki. The intended goal is to develop a body of formally represented and verified mathematics knowledge by using a community effort.
References
[1] Daniel Jackson. Alloy: a lightweight object modelling notation. Software Engineering and Methodology, 11(2):256–290, 2002.
[2] Fairouz Kamareddine and J. B. Wells. Computerizing mathematical text with mathlang. Electron. Notes Theor. Comput. Sci., 205:5–30, 2008.
[3] S. Owre, J. M. Rushby, , and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, jun 1992. Springer-Verlag.
[4] L. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994.
[5] Lawrence C. Paulson. Generic automatic proof tools. In Robert Veroff, editor, Automated Reasoning and Its Applications. MIT Press, 1997.
[6] Catherine Parent-Vigouroux. Verifying programs in the calculus of inductive constructions. Formal Aspects of Computing, 9(5-6):484–517, 1997.
[7] Dominik Dietrich, Ewaryst Schulz, and Marc Wagner. Authoring verified documents by interactive proof construction and verification in text-editors. In Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics, pages 398–414, Berlin, Heidelberg, 2008. Springer-Verlag.
[9] A. Abel, B. Chang, and F. Pfenning. Human-readable machine-verifiable proofs for teaching constructive logic, 2001.
[10] C. E. Brown. Verifying and Invalidating Textbook Proofs using Scunak. In Mathematical Knowledge Management, MKM 2006, page 110, Wokingham, England.
[11] D. Dietrich, E. Schulz, and M.Wagner. Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors. In Proceedings of the 9th AISC international conference, the 15th Calculemus symposium, and the 7th international MKM conference on Intelligent Computer Mathematics, pages 398–414, Berlin, Heidelberg, 2008. Springer-Verlag.
[12] D. McMath, M. Rozenfeld, and R. Sommer. A Computer Environment for Writing Ordinary Mathematical Proofs. In LPAR ’01: Proceedings of the Artificial Intelligence on Logic for Programming, pages 507–516, London, UK, 2001. Springer-Verlag.
[13] W. Sieg and S. Cittadini. Normal Natural Deduction Proofs (in Non-classical Logics). In D. Hutter andW. Stephan, editors, Mechanizing Mathematical Reasoning, volume 2605 of Lecture Notes in Computer Science, pages 169–191. Springer, 2005.
[14] K. Verchinine, A. Lyaletski, A. Paskevich, and A. Anisimov. On Correctness of Mathematical Texts from a Logical and Practical Point of View. In Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics, pages 583–598, Berlin, Heidelberg, 2008. Springer-Verlag.
[15] F. Wiedijk. Comparing mathematical provers. In MKM ’03: Proceedings of the Second International Conference on Mathematical Knowledge Management, pages 188– 202, London, UK, 2003. Springer-Verlag.
[16] Eric Allen, David Chase, Joe Hallett, Victor Luchangco, Jan-Willem Maessen, Sukyoung Ryu, Guy L. Steele Jr., and Sam Tobin-Hochstadt. The Fortress Language Specification Version 1.0. http://research.sun.com/projects/plrg/fortress.pdf, March 2008.
[17] Sukyoung Ryu. Parsing fortress syntax. In PPPJ '09: Proceedings of the 7th International Conference on Principles and Practice of Programming in Java, pages 76-84, New York, NY, USA, 2009. ACM.
[18] Konstantin Verchinine, Alexander Lyaletski, Andrei Paskevich, and Anatoly Anisimov. On Correctness of Mathematical Texts from a Logical and Practical Point of View. In Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics, pages 583-598, Berlin, Heidelberg, 2008. Springer-Verlag.
[19] Leo Bachmair and Ashish Tiwari. Abstract congruence closure and specializations. In CADE-17: Proceedings of the 17th International Conference on Automated Deduction, pages 64-78, London, UK, 2000. Springer-Verlag
[20] Greg Nelson and Derek C. Oppen. Fast decision procedures based on congruence closure. J. ACM, 27(2):356{364, 1980.
[21] Robert Nieuwenhuis and Albert Oliveras. Fast congruence closure and extensions. Inf. Comput., 205(4):557{580, 2007.
[22] Paul Cairns and Jeremy Gow. Integrating searching and authoring in mizar. J. Autom. Reason., 39(2):141{160, 2007.
[23] http://www.wolframalpha.com
[24] Neil Mitchell. Hoogle overview. The Monad.Reader, (12):27{35, November 2008.
[25] Sangmok Han, David R. Wallace, and Robert C. Miller. Code completion from abbreviated input, 2009.
[26] Greg Little and Robert C. Miller. Keyword programming in java, March 2009.
[27] Greg Little, Robert C. Miller, Victoria Chou, Michael Bernstein, Tessa Lau, and Allen Cypher. Sloppy Programming, 2009.
