Accessible Integrated Formal Reasoning Environments
From Accessible Integrated Formal Reasoning Environments
aartifact is a prototype infrastructure for defining, implementing, and maintaining user-accessible web-based integrated formal reasoning environments.
This infrastructure acts as a lightweight prototype that can be used to identify and provide a context for interesting problems related to practical integration of formal algorithms and systems. It is not an attempt to provide a universal language or system for formal reasoning assistance, or to supplant any existing syntax, interface, algorithm, or system.
In this context, formal reasoning refers to common formal reasoning tasks the semantics of which are already well-understood by a target community (e.g., the rules of algebraic manipulation are well-understood by most mathematicians). The investment non-expert users must make to involve existing algorithms and systems in such tasks remain non-trivial.
[edit] Motivation
Many automated formal reasoning and analysis techniques, tools, and systems have been developed by the formal verification, automated reasoning, and programming language research communities. The goal of this project is to assemble an infrastructure for instantiating accessible, web-based integrated environments that provide seamless, complementary ways to automate or assist common formal reasoning tasks that non-expert end-users encounter in their work in particular domains, both within research and classroom instruction.
Given a formal definition, model, or argument...
- ...what questions about it can be answered automatically?
- ...what techniques, algorithms, or underlying tools are appropriate for answering a particular question?
- ...what are the practical tradeoffs in choosing a particular technique over another in terms of cost, performance, soundness, and completeness?
- ...what is the appropriate way to interpret the result within the context of the definition, model, argument, or domain?
- ...what are the possible ways to extend or modify it in order to conform more closely to the ideal mental conception of the end-user?
- ...how should the user's expectations be modified to more closely conform to the limitations of mathematical modelling in general, or of specific techniques, algorithms, and underlying tools?
[edit] Development and maintenance
- Development
- Maintenance
[edit] Support and acknowledgements
This material is based upon work partially supported by the National Science Foundation under Grants No. 0820138 and No. 0720604. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.
This work is supported in part by the Hariri Institute at Boston University. Portions of this work represent efforts within the Church Project and the iBench Initiative, both located at the Boston University Computer Science Department.