A Function Elimination Method for Checking Satisfiability of Arithmetical Logics

• Autorzy: Castiglioni V. , Lanotte R. , Tini S.

Identyfikatory

DOI

10.3233/FI-2016-1303

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

satisfiability; arithmetic; mathematical formulas; problem solving; substitution

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 143, nr 1/2
• Strony: 51--71
• Opis fizyczny: Bibliogr. 40 poz.

Twórcy

autor

Castiglioni V.

• Department of Scienza e Alta Tecnologia University of Insubria, Italy

autor

Lanotte R.

• Department of Scienza e Alta Tecnologia University of Insubria, Italy

autor

Tini S.

• Department of Scienza e Alta Tecnologia University of Insubria, Italy

Bibliografia

• [1] Abdallah C. T., Dorato P., YangW., Liska R. and Steinberg S.: Applications of Quantifier Elimination Theory to Control System Design. Proc. IEEE Symp. on Control and Automation (1996), 340–345.
• [2] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P. H., Nicollin, X., Olivero, A., Sifakis, J. and Yovine, S.: The Algorithmic Analysis of Hybrid Systems. Theor. Comput. Sci. 138 (1995), 3–34.
• [3] Ash C.: Sentences with Finite Models.Weitschr. f. math. Logik u. Grundlagen d. Math. 21 (1975), 401– 404.
• [4] Börger E., Grädel E. and Gurevich Y.: The Classical Decision Problem. Springer (1997).
• [5] Castiglioni, V., Lanotte, R. and Tini, S.: A Function Elimination Method for Checking Satisfiability of Arithmetical Logics. Proc. Concurrency, Specification and Programming (2014), 46–57.
• [6] Davenport J. H. and Heintz, J.: Real Quantifier Elimination is Doubly Exponential. J. Symb. Comput. 5 (1988), 29–35.
• [7] Dolzmann A. and Sturm T.: Redlog: Computer Algebra Meets Computer Logic. ACM SIGSAM Bulletin 31 (1997), 2–9.
• [8] Dolzmann A., Sturm T. and Weispfenning V.: A New Approach for Automatic Theorem Proving in Real Geometry. J. Automated Reasoning 21 (1998), 357-380.
• [9] Downey P.: Undecidability of Presburger Arithmetic with a Single Monadic Predicate Letter. TR 18-72, Center for Research in Computing Technology, Harvard University (1972).
• [10] Enderton H. B.: Mathematical Introduction to Logic. Academic Press (1972).
• [11] Ferrante J. and Rackoff C.: A Decision Procedure for First-order Theory of Real Addition with Order. SIAM J. Comput. 4 (1975), 69–76.
• [12] Fischer M. J. and Rabin M. O.: Super-Exponential Complexity of Presburger Arithmetic. Complexity of Computation, SIAM-AMS Proc. 7 (1974), 27–42.
• [13] Godel K.: Ein Spezialfall des Entscheidungsproblems der theoretischen Logik. Ergebn. math. Kolloq. 2 (1932), 27–28.
• [14] Gurevich Y.: The Decision Problem for the Logic of Predicates and Operations. Algebra Logic 8 (1969), 160–174.
• [15] Gurevich Y.: Formulas with one ∀. Selected Questions in Algebra and Logics. Nauka (1973), 97–110.
• [16] Gurevich Y.: The Decision Problem for Standard Classes. J. Symbolic Comput. 41 (1976), 460–464.
• [17] Gurevich Y.: Monadic Second-order Theories. Model-theoretic Logics, Springer, Berlin (1985), 479–506.
• [18] Halpern J. Y.: Presburger Arithmetic with Unary Predicates is Π1 Complete. J.S.L. 56 (1991), 637–642.
• [19] HongaH. and Liskab R. (Eds.): Special Issue on Applications of Quantifier Elimination. J. Symbolic Comput. 24 (1997).
• [20] Kalmar L.: Uber die Erfullbarkeit derjenigen Zahlausdrucke, welehe in der Normalform zwei benachbarte Allzeichen enthalten. Math. Ann. 108 (1933), 466-484.
• [21] Lanotte, R.,Maggiolo-Schettini, A. and Tini, S.: Privacy in Real-Time Systems. Electr. Notes Theor. Comput. Sci. 52(3): 295-305 (2001).
• [22] Lanotte, R.,Maggiolo-Schettini,A., and Tini, S.: Information flow in hybrid systems. ACMTrans. Embedded Comput. Syst. 3(4): 760-799 (2004).
• [23] Lenstra H.W.: Integer Programming with a Fixed Number of Variables.Math. Oper. Res. 8 (1983), 538–548.
• [24] Löb M.: Decidability of The Monadic Predicate Calculus with Unary Function Symbols. J.S.L. 32(1967), 563.
• [25] Loos R., andWeipfenning V.: Applying Linear Quantifier Elimination. The Computer J. 36 (1993), 450–462.
• [26] Marker D.: Model Theory and Exponentiation. Notices AMS 43 (1996), 753–759.
• [27] Maslov S. and Orevkov V.: Decidable Classes Reducing to One-quantifier Class. Proc. Steklov Ins. Steklov Math 121 (1972), 61–72.
• [28] Matijasevic J. Y.: Hilbert’s Tenth Problem. MIT press, Cambridge (1993).
• [29] Rabin M.: Decidability of Second Order Theories and Automata on Infinite trees. Trans. Amer. Math. Soc. 141 (1969), 1–35.
• [30] Ramsey F. P.: On a Problem in Formal Logic. Proc. of the LondonMathematical Society 30 (1930), 264–286.
• [31] Schutte K.: Untersuchungen zum entscheidungsproblemder mathematischen logik.Math. Annal. 109 (1934), 572–603.
• [32] Shelah S.: The Monadic Theory of Order. Ann. of Math. 102 (1975), 379–419.
• [33] Shelah S.: Decidability of a Portion of the Predicate Calculus. Israel J. of Mathematics, 28 (1977), 32–44.
• [34] Shostak R. E.: A Practical Decision Procedure for Arithmetic with Functions Symbols. J. ACM 26 (1979), 351–360.
• [35] Subrami K.: An Analysis of Quantified Linear Programs. Proc. 4th Int. Conference on Discrete Mathematics and Theoretical Computer Science, Lecture and notes in Computer Science, 2731 (2003), Springer, 265–277.
• [36] Tarski A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951).
• [37] Thomas W.: Languages, Automata, and Logic. Handbook of Formal Languages, 3 (1997), 389–455.
• [38] Weispfenning V.: Mixed Real-Integer Linear Quantifier Elimination. Proc. ACMInt. Symp. on Symbolic and Algebraic Computation (1999).
• [39] Weispfenning V.: A New Approach to Quantifier Elimination for Real Algebra. In Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, Springer (1998).
• [40] Williams H. P.: Fourier-Motzkin Elimination Extension to Integer Programming. J. Comb. Theory 21 (1976), 118–123.