Automated Assistance for Formal Reasoning

From Automated Assistance for Formal Reasoning

This is an interactive demonstration of the aartifact automated assistant for interactive formal verification of human-accessible and machine-readable arguments involving fundamental concepts that are ubiquitous in mathematics and computer science. The aartifact system has two interfaces.

end-user interface	domain expert interface
The end-user interface allows users to author formal arguments; it provides lightweight validation feedback and syntax hints.	The domain expert interface allows domain experts to collaboratively assemble a database of formal facts governing domains.

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 .

Assume is a total function from to and is injective.

Assert for any , if then .

The aartifact automated assistant is generated in an automated manner from a static context (database) of common mathematical knowledge dealing with particular domains. This database can be collaboratively assembled and organized by experts using a dedicated interface. Together, the end-user interface, domain expert interface, and lightweight verification system constitute an automated assistant for formal reasoning. 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.

[edit] 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

[edit] 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.

• Propositional logic
• Propositional logic: more examples

[edit] Development and maintenance

• Development
  • Development: Task List
• Maintenance
  • Maintenance: Preparing an Amazon Web Services Instance
  • Maintenance: Integration with MediaWiki
  • Maintenance: Installing under Linux

[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.

Portions of this work represent efforts within the Church Project and the iBench Initiative, both located at the Boston University Computer Science Department.