Paper: Inductive Reasoning with Incomplete Specifications (Preliminary Report) (at LICS 1986)

Authors: Deepak Kapur David R. Musser

Abstract

An approach for proving a property by induction for incomplete (ambiguous) equational theories is presented. This approach extends the proof by consistency approach (related to the inductionless induction method) proposed by the authors for strongly complete (unambiguous) equational theories. A method for automating this approach using the Knuth and Bendix completion procedure is outlined. This method is based on transforming an incomplete equational theory into a strongly complete equantional theory in which theorems of the original incomplete theory remain theorems whereas equations which are independent axioms with respect to the original theory become inconsistent with the transformed strongly complete theory.

BibTeX

  @InProceedings{KapurMusser-InductiveReasoningw,
    author = 	 {Deepak Kapur and David R. Musser},
    title = 	 {Inductive Reasoning with Incomplete Specifications (Preliminary Report)},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {367--377},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }