We consider a proof procedure aiming at refuting clause sets containing arithmetic constants (or parameters), interpreted as natural numbers. The superposition calculus is enriched with a loop detection rule encoding a form of mathematical induction on the natural numbers (by “descente infinie”). This calculus and its theoretical properties are described in [2,16]. In the present paper, we focus on more practical aspects. We provide algorithms to apply the loop detection rule in an automatic and efficient way. We describe a research prototype implementing our technique and provide some preliminary experimental results.
展开▼
