A Complete Superposition Calculus for Primal Grammars

International audienceThe superposition calculus (Bachmair and Ganzinger, J. Log Comput. 3(4), 217–247, 1994; Nieuwenhuis and Rubio 1994) is the state-of-the-art inference system used in saturation-based theorem proving for first-order logic with equality.We present an extension of this calculus that permits us to reason on formulae built on primal grammars (Hermann and Galbavý, Theor. Comput. Sci. 176(1–2), 111–158, 1997) a schematization language that has been devised to denote infinite sequences of structurally similar terms, defined by primitive recursion. We prove that the calculus is sound and refutationally complete