2017/05/24 by Dawn Michaelson, Michaelson, Dawn
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1705.09025
openalex publication_date 2017/05/24 · openalex created_date 2023/03/14 · openalex updated_date 2026/07/28
In logical reasoning, it is often the case that only some of a collection of\nassumptions are needed to reach a conclusion. A strengthening lemma is an\nassertion that a given conclusion is independent in this sense of a particular\nassumption. Strengthening lemmas underlie many useful techniques for\nsimplifying proofs in automated and interactive theorem-provers. For example,\nthey underlie a mechanism called subordination that is useful in determining\nthat expressions of a particular type cannot contain objects of another type\nand in thereby reducing the number of cases to be considered in proving\nuniversally quantified statements.\n This thesis concerns the automation of the proofs of strengthening lemmas in\na specification logic called the logic of hereditary Harrop formulas (HOHH).\nThe Abella Proof Assistant embeds this logic in a way that allows it to prove\nproperties of both the logic itself and of specifications written in it.\nPrevious research has articulated a (conservative) algorithm for checking if a\nclaimed strengthening lemma is, in fact, true. We provide here an\nimplementation of this algorithm within the setting of Abella. Moreover, we\nshow how to generate an actual proof of the strengthening lemma in Abella from\nthe information computed by the algorithm; such a proof serves as a more\ntrustworthy certificate of the correctness of the lemma than the algorithm\nitself. The results of this work have been incorporated into the Abella system\nin the form of a "tactic command" that can be invoked within the interactive\ntheorem-prover and that will result in an elaboration of a proof of the lemma\nand its incorporation into the collection of proven facts about a given\nspecification.\n