MURAL - Maynooth University Research Archive Library

    Creating new Program Proofs by Combining Abductive and Deductive Reasoning

    Ajankovil, Kuruvilla George and O'Donoghue, Diarmuid and Monahan, Rosemary (2021) Creating new Program Proofs by Combining Abductive and Deductive Reasoning. In: International Conference on Computational Creativity ICCC, September 2021.

    Download (762kB) | Preview

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    We describe recent work on the Aris system that creates and verifies new formal specifications for pre-existing source code. We describe Aris in terms of the abductive reasoning system that suggest possible specifications and then uses an existing deductive verifier to evaluate these creations. This paper focuses on the abduction system that creates new formal specifications by leveraging a small set of inspiring artefacts to augment a subset of candidate problems. This employs knowledge graphs to represent the raw data (i.e., source code), discovering latent similarities between graphs using a graph-matching process. Results are presented for the C# programming language with novel creations and its sister language called Code Contracts. We outline ampliative creativity, whereby newly created artefacts drive subsequent creative episodes beyond the initially perceived limitations. We also outline some recent work towards transferring specifications between the C# and Java programming languages.

    Item Type: Conference or Workshop Item (Paper)
    Keywords: Creating; new Program Proofs; Combining Abductive; Deductive Reasoning;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Faculty of Science and Engineering > Research Institutes > Hamilton Institute
    Item ID: 15752
    Depositing User: Dr. Diarmuid O'Donoghue
    Date Deposited: 29 Mar 2022 15:28
    Refereed: Yes
    Use Licence: This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

    Repository Staff Only(login required)

    View Item Item control page


    Downloads per month over past year

    Origin of downloads