Automated Assistance for Formal Reasoning
From Automated Assistance for Formal Reasoning
This is a repository for human-accessible and machine-comprehensible formal arguments written in a combination of LaTeX syntax and English phrases, as illustrated in the example below. This instance of MediaWiki has been augmented with the aartifact automated assistant for formal reasoning, which allows users to perform lightweight validation on their proofs as they are editing. To validate formal arguments, simply click the Verify button at the bottom of the Edit page of any article.
- Introduce f.
- Assume f is a total function from
to and f is injective.
- Assert for any
, if 
then 
.
The aartifact automated assistant is generated in an automated manner from a rich static context of common mathematical knowledge dealing with particular domains. Together, the aartifact system and the static context constitute a sophisticated formal reasoning interface for verification tools. The purpose of this interface is to support semantic machine comprehension of formal reasoning as it is practiced by human users. It is the hope of the designers that the tools and ideas presented here can lead to improvements in the interface design and user accessibility of both well-established and future formal reasoning and verification systems.
In addition to the static context interface, a short tutorial covering the top-level syntax is available, as well as a background, motivation, and discussion that includes references to related work. A summary of relevant documents and literature has pointers to technical reports and presentation slides.
Up-to-date examples
- Irrationality of the square root of two
- Finite ranges of integers
- Inference of scheduling transformations
- Induction proofs for functional code
- Vector space example
Uncategorized site map
Older pages not currently being maintained may contain outdated or incompatible examples.
Support and acknowledgements
This material is based upon work partially supported by the National Science Foundation under Grant No. 0820138. 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.
