A general Framework to Build Contextual Cover Set Induction Provers

摘要

Cover set induction is known as a proof method that keeps the advantages of explicit induction and proof by consistency. Most implicit induction proof procedures are defined in a cover set induction framework. Contextual cover set (CCS) is a new concept that fully characterizes explicit induction schemes, such as the cover sets, and many simpli- fication techniques as those specific to the " proof by consistency" approach. Firstly, we present an abstract inference system uniformly defined in terms of contextual cover sets as our general framework to build implicit induction provers.