First-Order Polynomial Based Theorem Proving

Introduction The Boolean ring or first-order polynomial based theorem proving began with the work of Hsiang (1982, 1985). Hsiang extended the idea of using Boolean polynomials to represent propositional formulae to the case of first-order predicate calculus. Based on the completion procedure of Knuth and Bendix (1970), the N-strategy was proposed. Later on, by imitating the framework of Buchberger 's algorithm to compute the Grobner bases of polynomial ideals (Buchberger 1985), Kapur and Narendran (1985) developed another approach which is also referred to as the Grobner basis method. One obvious advantage of using Boolean polynomials is that every propositional formula has a unique representation, and sometimes it is easy to be generalized to some non-classical logic systems (Chazarain et al. 1991; Wu and Tan 1994). Stimulated by them, some approaches and results have been reported (Bachmair and Dershowitz 1987; Dietrich 1986; Kapur and Zhang 1989; Wu and Liu 1998; Zhang 19