Automated Assistance for Formal Reasoning
From Automated Assistance for Formal Reasoning
This is an interactive demonstration of the aartifact automated assistant for formal verification of human-accessible and machine-readable arguments involving fundamental concepts that are ubiquitous in mathematics and computer science. This instance of MediaWiki is augmented to let users perform lightweight validation of their arguments while editing. Arguments are written using LaTeX syntax and English phrases, as illustrated in the example below. 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. 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 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 list of reports and documents has pointers to technical reports and presentation slides, and there is a high-level summary of future directions for this work.
Examples requiring the full static context
- Irrationality of the square root of two
- Infinitude of primes
- Algebra of sets
- Finite ranges of integers
- Inference of scheduling transformations
- Basic induction over natural numbers
- Induction proofs for functional code
- Vector space example
Propositional logic
Because the dynamic context computes congruence closures, it can be used to support verification of formal arguments that only utilize propositional logic. Select the propositional logic option before clicking Verify.
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 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.
