A Function Elimination Method for Checking Satisfiability of Arithmetical Logics

Issue title: Concurrency, Specification and Programming (CS&P)

Guest editors: Ludwik Czaja, Wojciech Penczek and Krzysztof Stencel

Article type: Research Article

Authors: Castiglioni, Valentina^* | Lanotte, Ruggero | Tini, Simone

Affiliations: Department of Scienza e Alta Tecnologia, University of Insubria, Italy. simone.tini@uninsubria.it, ruggero.lanotte@uninsubria.it

Correspondence: [*] Address for correspondence: Department of Scienza e Alta Tecnologia, University of Insubria, Via Valleggio 11, I-22100, Como, Italy

Abstract: 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 formulas allowing linear and polynomial terms.

DOI: 10.3233/FI-2016-1303

Journal: Fundamenta Informaticae, vol. 143, no. 1-2, pp. 51-71, 2016