Consistency checking for automatic software generation

This paper presents a new formal approach to checking consistency of a set of axioms that define a function. Our approach is an alternative to the original knuth-bendix (KB) completion procedure which can only process equational axioms. Additional steps are required to be implemented in KB in order to use it with conditional equations which are heavily used as function specifications. Since the size of the code to be trusted is important in systems like Code-carrying theory and Proof-carrying code, it is also important to have a short implementation. We show that our alternative idea is simpler and easy to implement with a small amount of code. In addition, our approach does not require one to define a well-founded ordering relation as in knuth-bendix procedure making it more practical to use it with less effort.