A Function Elimination Method for Checking Satisfiability of Arithmetical Logics
Valentina Castiglioni, Ruggero Lanotte, Simone Tini · Fundamenta Informaticae · 2016
We study function elimination for Arithmetical Logics. We propose a method allowing substitution of functions occurring in a given formula with functions with less arity. We prove the correctness of the method and we use it to show the decidability of the satisfiability problem for two classes of f ormulas allowing linear and polynomial terms.