Automating the Proofs of Strengthening Lemmas in the Abella Proof Assistant

Michaelson, Dawn
2017
Thumbnail Image

View/Download File

Dawn Michaelson summa CSE sp2017.pdf (346.15 KB)

Persistent link to this item

https://hdl.handle.net/11299/189106
Statistics
View Statistics

Journal Title

Journal ISSN

Volume Title

Title

Automating the Proofs of Strengthening Lemmas in the Abella Proof Assistant

Authors

Published Date

2017

Publisher

Type

Thesis or Dissertation

Abstract

In logical reasoning, it is often the case that only some of a collection of assumptions are needed to reach a conclusion. A strengthening lemma is an assertion that a given conclusion is independent in this sense of a particular assumption. Strengthening lemmas underlie many useful techniques for simplifying proofs in automated and interactive theorem-provers. For example, they underlie a mechanism called subordination that is useful in determining that expressions of a particular type cannot contain objects of another type and in thereby reducing the number of cases to be considered in proving universally quanti ed statements. This thesis concerns the automation of the proofs of strengthening lemmas in a speci cation logic called the logic of hereditary Harrop formulas (HOHH). The Abella Proof Assistant embeds this logic in a way that allows it to prove properties of both the logic itself and of speci cations written in it. Previous research has articulated a (conservative) algorithm for checking if a claimed strengthening lemma is, in fact, true. We provide here an implementation of this algorithm within the setting of Abella. Moreover, we show how to generate an actual proof of the strengthening lemma in Abella from the information computed by the algorithm; such a proof serves as a more trustworthy certifi cate of the correctness of the lemma than the algorithm itself. The results of this work have been incorporated into the Abella system in the form of a \tactic command" that can be invoked within the interactive theorem-prover and that will result in an elaboration of a proof of the lemma and its incorporation into the collection of proven facts about a given speci cation.

Keywords

Description

Related to

Replaces

License

Collections

Undergraduate Honors Theses

Series/Report Number

Funding information

Isbn identifier

Doi identifier

Previously Published Citation

Suggested citation

Michaelson, Dawn. (2017). Automating the Proofs of Strengthening Lemmas in the Abella Proof Assistant. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/189106.

Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.