Dei: A Theorem Prover for Terms with Integer Exponents

Abstract. An extension of the superposition-based E-prover [8] is described. The extension allows terms with integer exponents [3] in the input language. Obviously, this possibility increases the capabilities of the E-prover particularly for preventing non-termination.

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
• Keywords: Automated Reasoning, CADE 2009, Extension Allows Terms