Proof Learning in PVS with Utility Pattern Mining
Article
Article Title | Proof Learning in PVS with Utility Pattern Mining |
---|---|
ERA Journal ID | 210567 |
Article Category | Article |
Authors | Nawaz, M. Saqib (Author), Fournier-Viger, Philippe (Author) and Zhang, Ji (Author) |
Journal Title | IEEE Access |
Journal Citation | 8, pp. 119806-119818 |
Article Number | 9122488 |
Number of Pages | 13 |
Year | 2020 |
Publisher | IEEE (Institute of Electrical and Electronics Engineers) |
Place of Publication | United States |
ISSN | 2169-3536 |
Digital Object Identifier (DOI) | https://doi.org/10.1109/ACCESS.2020.3004199 |
Web Address (URL) | https://ieeexplore.ieee.org/abstract/document/9122488 |
Abstract | Interactive theorem provers (ITPs) are software tools that allow human users to write and verify formal proofs. In recent years, an emerging research area in ITPs is proof mining, which consists of identifying interesting proof patterns that can be used to guide the interactive proof process in ITPs. In previous studies, some data mining techniques, such as frequent pattern mining, have been used to analyze proofs to find frequent proof steps. Though useful, such models ignore the facts that not all proof steps are equally important. To address this issue, this paper proposes a novel proof mining approach based on finding not only frequent patterns but also high utility patterns to find proof steps of high importance (utility). A proof process learning approach is proposed based on high utility itemset mining (HUIM) for the PVS (Prototype Verification System) proof assistant. Proofs in PVS theories are first abstracted to a computer-processable corpus, where each line represents a proof sequence and proof commands in proof sequences are associated with utilities representing their weightage (importance). HUIM techniques are then applied on the corpus to discover frequent proof steps/high utility patterns and their relationships with each other. Experimental results suggest that combining frequent pattern mining techniques, such as sequential pattern mining and high utility itemset mining, with proof assistants, such as PVS, is useful to learn and guide the proof development process. |
Keywords | Frequent patterns, high utility itemset mining, proof steps, proof sequences, PVS |
ANZSRC Field of Research 2020 | 460502. Data mining and knowledge discovery |
Byline Affiliations | Harbin Institute of Technology, China |
School of Sciences | |
Open access url | https://ieeexplore.ieee.org/abstract/document/9122488 |
Institution of Origin | University of Southern Queensland |
https://research.usq.edu.au/item/q63w9/proof-learning-in-pvs-with-utility-pattern-mining
Download files
Published Version
Nawaz-2020-Proof-learning-in-pvs-with-utility-.pdf | ||
License: CC BY 4.0 | ||
File access level: Anyone |
134
total views64
total downloads3
views this month2
downloads this month