Stefan Hetzl ; Tin Lok Wong - Some observations on the logical foundations of inductive theorem proving

lmcs:3256 - Logical Methods in Computer Science, April 13, 2018, Volume 13, Issue 4 - https://doi.org/10.23638/LMCS-13(4:10)2017
Some observations on the logical foundations of inductive theorem provingArticle

Authors: Stefan Hetzl ORCID; Tin Lok Wong

    In this paper we study the logical foundations of automated inductive theorem proving. To that aim we first develop a theoretical model that is centered around the difficulty of finding induction axioms which are sufficient for proving a goal. Based on this model, we then analyze the following aspects: the choice of a proof shape, the choice of an induction rule and the language of the induction formula. In particular, using model-theoretic techniques, we clarify the relationship between notions of inductiveness that have been considered in the literature on automated inductive theorem proving.

    https://doi.org/10.23638/LMCS-13(4:10)2017
    Source: arXiv.org:1704.01930
    Volume: Volume 13, Issue 4
    Section: Automated deduction
    Published on: April 13, 2018
    Accepted on: November 2, 2017
    Submitted on: September 5, 2017
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic
    Licence: Attribution 4.0 International (CC BY 4.0)
    Funding:
      Source : OpenAIRE Graph
    • The Infinity Project; Code: P 24654

    Share and export

    Consultation statistics

    This page has been seen 2197 times.
    This article's PDF has been downloaded 774 times.