Automatic synthesis of logical models for order-sorted first-order theories. (English) Zbl 1398.68095
Summary: In program analysis, the synthesis of models of logical theories representing the program semantics is often useful to prove program properties. We use order-sorted first-order logic as an appropriate framework to describe the semantics and properties of programs as given theories. Then we investigate the automatic synthesis of models for such theories. We use convex polytopic domains as a flexible approach to associate different domains to different sorts. We introduce a framework for the piecewise definition of functions and predicates. We develop its use with linear expressions (in a wide sense, including linear transformations represented as matrices) and inequalities to specify functions and predicates. In this way, algorithms and tools from linear algebra and arithmetic constraint solving (e.g., SMT) can be used as a backend for an efficient implementation.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 03B70 | Logic in computer science |
References:
| [1] | Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of AMAST’10. LNCS, vol. 6486, pp. 201-208 (2011) · Zbl 1308.68068 |
| [2] | Alarcón, B., Lucas, S., Navarro-Marset, R.: Using matrix interpretations over the reals in proofs of termination. In: Proceedings of PROLE’09, pp. 255-264 (2009) |
| [3] | Albert, E., Genaim, S., Gutiérrez, R.: A Transformational Approach to Resource Analysis with Typed-Norms. Revised Selected Papers from LOPSTR’13. LNCS, vol. 8901, pp 38-53 (2013) · Zbl 1453.68041 |
| [4] | Angelis, E; Fioravante, F; Pettorossi, A; Proietti, M, Proving correctness of imperative programs by linearizing constrained Horn clauses, Theory Pract. Log. Program., 15, 635-650, (2015) · Zbl 1379.68093 · doi:10.1017/S1471068415000289 |
| [5] | de Angelis, E., Fioravante, F., Pettorossi, A., Proietti, M.: Semantics-based generation of verification conditions by program specialization. In: Proceedings of PPDP’15, pp. 91-102. ACM Press, New York (2015) |
| [6] | Aoto, T, Solution to the problem of zantema on a persistent property of term rewriting systems, J. Funct. Log. Program., 2001, 1-20, (2001) · Zbl 1037.68066 |
| [7] | Barwise, J; Barwise, J (ed.), An introduction to first-order logic, (1977), Amsterdam · Zbl 0216.00305 |
| [8] | Barwise, J, Axioms for abstract model theory, Ann. Math. Log., 7, 221-265, (1974) · Zbl 0324.02034 · doi:10.1016/0003-4843(74)90016-3 |
| [9] | Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry. Springer, Berlin (1998) · Zbl 0912.14023 · doi:10.1007/978-3-662-03718-8 |
| [10] | Birkhoff, G; Lipson, JD, Heterogeneous algebras, J. Comb. Theory, 8, 115-133, (1970) · Zbl 0211.02003 · doi:10.1016/S0021-9800(70)80014-X |
| [11] | Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: The Barcelogic SMT Solver. In: Proceedings of CAV’08. LNCS, vol. 5123, pp. 294-298 (2008) |
| [12] | Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn-clause solvers for program verification. In: Fields of Logic and Computation II—Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. LNCS, vol. 9300, pp. 24-51 (2015) · Zbl 1465.68044 |
| [13] | Bjørner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn-clauses. In: Proceedings of SAS’13. LNCS vol. 7935, pp. 105-125 (2013) |
| [14] | Bjørner, N., McMillan, K., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: Proceedings of SMT’12, EPiC Series in Computing, vol. 20, pp. 3-11 (2013) · Zbl 0211.02003 |
| [15] | Bliss, G.A.: Algebraic Functions. Dover (2004) |
| [16] | Bonfante, G., Marion, J.-Y., Moyen, J.-Y.: On Lexicographic Termination Ordering With Space Bound Certifications. Revised Papers from PSI 2001. LNCS, vol. 2244, pp. 482-493 (2001) · Zbl 1073.68561 |
| [17] | Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 4th edn. Cambridge University Press, Cambridge (2002) · Zbl 1014.03001 · doi:10.1017/CBO9781139164931 |
| [18] | Borralleras, C; Lucas, S; Oliveras, A; Rodríguez, E; Rubio, A, SAT modulo linear arithmetic for solving polynomial constraints, J. Autom. Reason., 48, 107-131, (2012) · Zbl 1243.68210 · doi:10.1007/s10817-010-9196-8 |
| [19] | Bürckert, H-J; Hollunder, B; Laux, A, On skolemization in constrained logics, Ann. Math. Artif. Intell., 18, 95-131, (1996) · Zbl 0887.03005 · doi:10.1007/BF02127744 |
| [20] | Burstall, R.M., Goguen, J.A.: Putting Theories together to make specifications. In: Proceedings of IJCAI’77, pp. 1045-1058. William Kaufmann (1977) |
| [21] | Caplain, M.: Finding invariant assertions for proving programs. In: Proceedings of the International Conference on Reliable Software, pp. 165-171. ACM Press, New York (1975) · JFM 64.0028.01 |
| [22] | Chang, C.L., Lee, R.C.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, Orlando (1973) · Zbl 0263.68046 |
| [23] | Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude—A High-Performance Logical Framework. LNCS 4350, (2007) · Zbl 1115.68046 |
| [24] | Cohn, A.G.: Improving the expressiveness of many sorted logic. In: Proceedings of the National Conference on Artificial Intelligence, pp. 84-87. AAAI Press, Menlo Park (1983) |
| [25] | Contejean, E; Marché, C; Tomás, A-P; Urbain, X, Mechanically proving termination using polynomial interpretations, J. Autom. Reason., 34, 325-363, (2006) · Zbl 1108.03017 · doi:10.1007/s10817-005-9022-x |
| [26] | Cooper, DC, Programs for mechanical program verification, Mach. Intell., 6, 43-59, (1971) · Zbl 0261.68023 |
| [27] | Cooper, DC, Theorem proving in arithmetic without multiplication, Mach. Intell., 7, 91-99, (1972) · Zbl 0258.68046 |
| [28] | Courtieu, P., Gbedo, G., Pons, O.: Improved matrix interpretations. In: Proceedings of SOFSEM’10. LNCS, vol. 5901, pp. 283-295 (2010) · Zbl 1274.68148 |
| [29] | Cousot, P., Cousot, R., Mauborgne, L.: Logical abstract domains and interpretations. In: The Future of Sofware Engineering, pp. 48-71. Springer, New York (2011) · Zbl 1326.68089 |
| [30] | Cousot, P., Halbwachs, N.: Automatic Discovery of linear restraints among variables of a program. In: Conference Record of POPL’78, pp. 84-96. ACM Press, New York (1978) · Zbl 0810.68087 |
| [31] | Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990) · Zbl 0701.06001 |
| [32] | Elspas, B; Levitt, KN; Waldinger, RJ; Waksman, A, An assessment of techniques for proving program correctness, Comput. Surv., 4, 97-147, (1972) · Zbl 0266.68010 · doi:10.1145/356599.356602 |
| [33] | Emdem, MH; Kowalski, RA, The semantics of predicate logic as a programming language, J. ACM, 23, 733-742, (1976) · Zbl 0339.68004 · doi:10.1145/321978.321991 |
| [34] | Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. In: Proceedings of IJCAR’06. LNCS, vol. 4130, pp. 574-588 (2006) · Zbl 1222.68362 |
| [35] | Endrullis, J; Waldmann, J; Zantema, H, Matrix interpretations for proving termination of term rewriting, J. Autom. Reason., 40, 195-220, (2008) · Zbl 1139.68049 · doi:10.1007/s10817-007-9087-9 |
| [36] | Floyd, RW, Assigning meanings to programs, Math. Asp. Comput. Sci., 19, 19-32, (1967) · Zbl 0189.50204 · doi:10.1090/psapm/019/0235771 |
| [37] | Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: Proceedings of RTA’08. LNCS, vol. 5117, pp. 110-125 (2008) · Zbl 1145.68446 |
| [38] | Fuhs, C; Giesl, J; Parting, M; Schneider-Kamp, P; Swiderski, S, Proving termination by dependency pairs and inductive theorem proving, J. Autom. Reason., 47, 133-160, (2011) · Zbl 1243.68267 · doi:10.1007/s10817-010-9215-9 |
| [39] | Fuhs, C., Kop, C.: Polynomial interpretations for higher-order rewriting. In: Proceedings of RTA’12. LIPIcs, vol. 15, pp. 176-192 (2012) · Zbl 0324.02034 |
| [40] | Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, AMAST Series, (1998) · Zbl 0962.68115 |
| [41] | Gaboardi, M; Péchoux, R, On bounding space usage of streams using interpretation analysis, Sci. Comput. Program., 111, 395-425, (2015) · doi:10.1016/j.scico.2015.05.004 |
| [42] | Giesl, J., Mesnard, F., Rubio, A., Thiemann, R., Waldmann, J.: Termination competition (termCOMP 2015). In: Proceedings of CADE’15. LNCS, vol. 9195, pp. 105-108 (2015) · Zbl 1465.68282 |
| [43] | Giesl, J., Ströder, T., Schneider-Kamp, P., Emmes, F., Fuhs, C.: Symbolic evaluation graphs and term rewriting—a general methodology for analyzing logic programs. In: Proceedings of the PPDP’12, pp. 1-12. ACM Press (2012) |
| [44] | Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33(2), 7 (2011) · Zbl 1151.68444 |
| [45] | Gnaedig, I.: Termination of Order-sorted Rewriting. In: Proceedings of ALP’92. LNCS, vol. 632, pp. 37-52 (1992) |
| [46] | Goguen, J.A.: Order-Sorted Algebra. Semantics and Theory of Computation Report 14, UCLA (1978) |
| [47] | Goguen, JA; Burstall, RM, Some fundamental algebraic tools for the semantics of computation. part 1: comma categories, colimits, signatures and theories, Theoret. Comput. Sci., 31, 175-209, (1984) · Zbl 0566.68065 · doi:10.1016/0304-3975(84)90134-8 |
| [48] | Goguen, JA; Burstall, RM, Some fundamental algebraic tools for the semantics of computation. part 2 signed and abstract theories, Theoret. Comput. Sci., 31, 263-295, (1984) · Zbl 0566.68066 · doi:10.1016/0304-3975(84)90036-7 |
| [49] | Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Proceedings of TAPSOFT’87. LNCS, vol. 250, pp. 1-22 (1987) · Zbl 0626.68032 |
| [50] | Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Current Trends in Programming Methodology, pp. 80-149. Prentice Hall (1978) |
| [51] | Goguen, JA; Meseguer, J, Remarks on remarks on many-sorted equational logic, Sigplan Notices, 22, 41-48, (1987) · Zbl 1023.68630 · doi:10.1145/24714.24719 |
| [52] | Goguen, J; Meseguer, J, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoret. Comput. Sci., 105, 217-273, (1992) · Zbl 0778.68056 · doi:10.1016/0304-3975(92)90302-V |
| [53] | Goguen, JA; Winkler, T; Meseguer, J; Futatsugi, K; Jouannaud, J-P; Goguen, J (ed.); Malcolm, G (ed.), Introducing OBJ, (2000), Boston · doi:10.1007/978-1-4757-6541-0 |
| [54] | Grebenshikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Proceedings of PLDI’12, pp. 405-416. ACM Press (2012) · Zbl 0198.22001 |
| [55] | Gulwani, S., Tiwari, A.: Combining Abstract Interpreters. In: Proceedings of PLDI’06, pp. 376-386. ACM Press (2006) |
| [56] | Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Proceedings of CAV’15, Part I. LNCS, vol. 9206, pp. 343-361 (2015) · Zbl 0285.68011 |
| [57] | Gutiérrez, R., Lucas, S., Reinoso, P.: A tool for the automatic generation of logical models of order-sorted first-order theories. In: Proceedings of PROLE’16, pp. 215-230 (2016). http://zenon.dsic.upv.es/ages/ |
| [58] | Hantler, SL; King, JC, An introduction to proving the correctness of programs, ACM Comput. Surv., 8, 331-353, (1976) · Zbl 0345.68009 · doi:10.1145/356674.356677 |
| [59] | Hayes, P, A logic of actions, Mach. Intell., 6, 495-520, (1971) · Zbl 0268.68039 |
| [60] | Heidergott, B., Olsder, G.J., van der Woude, J.: Max plus at work. A course on max-plus algebra and its applications. In: Modeling and Analysis of Synchronized Systems, Princeton University Press (2006) · Zbl 1130.93003 |
| [61] | Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Proceedings of IJCAR 2008. LNCS, vol. 5195, pp. 364-379 (2008) · Zbl 1165.68390 |
| [62] | Hoare, CAR, An axiomatic basis for computer programming, Commun. ACM, 12, 576-583, (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259 |
| [63] | Hodges, W.: Elementary Predicate Logic. Handbook of Philosophical Logic, vol. 1, pp. 1-131. Reidel Publishing Company (1983) · Zbl 0875.03035 |
| [64] | Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge (1997) · Zbl 0873.03036 |
| [65] | Hofbauer, D.: Termination proofs by context-dependent interpretation. In: Proceedings of RTA’01. LNCS, vol. 2051, pp. 108-121 (2001) · Zbl 0981.68068 |
| [66] | Hofbauer, D, Termination proofs for ground rewrite systems. interpretations and derivational complexity, Appl. Algebra Eng. Commun. Comput., 12, 21-38, (2001) · Zbl 0973.68100 · doi:10.1007/s002000100062 |
| [67] | Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Proceedings of RTA’89. LNCS, vol. 355, pp. 167-177 (1989) · Zbl 1503.68116 |
| [68] | Hull, T.E., Enright, W.H., Sedgwick, A.E.: The correctness of numerical algorithms. In: Proceedings of PAAP’72, pp. 66-73 (1972) · Zbl 0353.68016 |
| [69] | Igarashi, S; London, RL; Luckham, D, Automatic program verification I: a logical basis and its implementation, Acta Inform., 4, 145-182, (1975) · Zbl 0279.68022 · doi:10.1007/BF00288746 |
| [70] | Iwami, M.: Persistence of termination of term rewriting systems with ordered sorts. In: Proceedings of 5th JSSST Workshop on Programming and Programming Languages, Shizuoka, Japan, pp. 47-56. (2003) |
| [71] | Iwami, M.: Persistence of termination for non-overlapping term rewriting systems. In: Proceedings of Algebraic Systems, Formal Languages and Conventional and Unconventional Computation Theory, Kokyuroku RIMS, University of Kyoto, vol. 1366, pp. 91-99 (2004) · Zbl 0279.68022 |
| [72] | Katz, S; Manna, Z, Logical analysis of programs, Commun. ACM, 19, 188-206, (1976) · Zbl 0353.68016 · doi:10.1145/360032.360048 |
| [73] | Langford, CH, Review: über deduktive theorien mit mehreren sorten von grunddingen, J. Symb. Log., 4, 98, (1939) · doi:10.2307/2269080 |
| [74] | Lankford, D.S.: Some approaches to equality for computational logic: a survey and assessment. Memo ATP-36, Automatic Theorem Proving Project, University of Texas, Austin, TX · Zbl 0973.68100 |
| [75] | London, R.L.: The current state of proving programs correct. In: Proceedings of ACM’72, vol. 1, pp. 39-46. ACM (1972) |
| [76] | Lucas, S, Polynomials over the reals in proofs of termination: from theory to practice, RAIRO Theor. Inform. Appl., 39, 547-586, (2005) · Zbl 1085.68076 · doi:10.1051/ita:2005029 |
| [77] | Lucas, S, Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving, Electron. Proc. Theor. Comput. Sci., 200, 32-47, (2015) · doi:10.4204/EPTCS.200.3 |
| [78] | Lucas, S.: Use of logical models for proving operational termination in general logics. In: Selected Papers from WRLA’16. LNCS, vol. 9942, pp. 1-21 (2016) · Zbl 1367.68068 |
| [79] | Lucas, S; Marché, C; Meseguer, J, Operational termination of conditional term rewriting systems, Inform. Proces. Lett., 95, 446-453, (2005) · Zbl 1185.68374 · doi:10.1016/j.ipl.2005.05.002 |
| [80] | Lucas, S., Meseguer, J.: Models for logics and conditional constraints in automated proofs of termination. In: Proceedings of AISC’14. LNAI, vol. 8884, pp. 7-18 (2014) |
| [81] | Lucas, S., Meseguer, J.: Order-sorted dependency pairs. In: Proceedings of PPDP’08 , pp. 108-119. ACM Press (2008) |
| [82] | Lucas, S., Meseguer, J.: Proving operational termination of declarative programs in general logics. In: Proceedings of PPDP’14, pp. 111-122. ACM Digital Library (2014) · Zbl 0345.68009 |
| [83] | Lucas, S; Meseguer, J, Dependency pairs for proving termination properties of conditional term rewriting systems, J. Log. Algebr. Methods Program., 86, 236-268, (2017) · Zbl 1353.68155 · doi:10.1016/j.jlamp.2016.03.003 |
| [84] | Manna, Z, The correctness of programs, J. Comput. Syst. Sci., 3, 119-127, (1969) · Zbl 0285.68011 · doi:10.1016/S0022-0000(69)80009-7 |
| [85] | Manna, Z, Properties of programs and the first-order predicate calculus, J. ACM, 16, 244-255, (1969) · Zbl 0198.22001 · doi:10.1145/321510.321516 |
| [86] | Manna, Z.: Termination of programs represented as interpreted graphs. In: Proceedings of AFIPS’70, pp. 83-89 (1970) |
| [87] | Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proceedings of the Third Hawaii International Conference on System Science, pp. 789-792 (1970) |
| [88] | Manna, Z; Pnueli, A, Formalization of properties of functional programs, J. ACM, 17, 555-569, (1970) · Zbl 0206.17503 · doi:10.1145/321592.321606 |
| [89] | Marion, Y-I; Péchoux, R, Sup-interpretations, a semantic method for static analysis of program resources, ACM Trans. Comput. Log., 10, 27, (2009) · Zbl 1351.68061 · doi:10.1145/1555746.1555751 |
| [90] | Martí-Oliet, N., Meseguer, J., Palomino, M.: Theoroidal maps as algebraic simulations. Revised Selected Papers from WADT’04. LNCS, vol. 3423, pp. 126-143 (2005) · Zbl 1119.68129 |
| [91] | McCarthy, J, Recursive functions of symbolic expressions and their computation by machine. part I, Commun. ACM, 3, 184-195, (1960) · Zbl 0101.10413 · doi:10.1145/367177.367199 |
| [92] | Meseguer, J.: General logics. In: Ebbinghaus, H.D., et al. (eds.) Logic Colloquium’87, pp. 275-329. North-Holland (1989) · Zbl 0691.03001 |
| [93] | Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. Revised Selected Papers from LOPSTR’15. LNCS, vol. 9527, pp. 36-53 (2015) · Zbl 1362.68053 |
| [94] | Middeldorp, A.: Matrix interpretations for polynomial derivational complexity of rewrite systems. In: Proceedings of LPAR’12. LNCS, vol. 7180, p. 12 (2012) |
| [95] | Monin, J.-F.: Understanding Formal Methods. Springer, London (2003) · Zbl 1013.68119 · doi:10.1007/978-1-4471-0043-0 |
| [96] | Montenegro, M; Peña, R; Segura, C, Space consumption analysis by abstract interpretation: inference of recursive functions, Sci. Comput. Program., 111, 426-457, (2015) · doi:10.1016/j.scico.2014.04.006 |
| [97] | Moura, L; Bjørner, N, Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 69-77, (2011) · doi:10.1145/1995376.1995394 |
| [98] | Naur, P, Proof of algorithms by general snapshots, Bit, 6, 310-316, (1966) · doi:10.1007/BF01966091 |
| [99] | Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewriting. In: Proceedings of RTA’11. LIPICS, vol. 10, pp. 251-266 (2011) · Zbl 1236.68141 |
| [100] | Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002) · Zbl 0999.68095 · doi:10.1007/978-1-4757-3661-8 |
| [101] | Ölveczky, P.C., Lysne, O.: Order-sorted termination: the unsorted way. In: Proceedings of ALP’96. LNCS, vol. 1139, pp. 92-106 (1996) · Zbl 1355.68134 |
| [102] | Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of java bytecode by term rewriting. In: Proceedings of RTA’10. LIPICS, vol. 6, pp. 259-276 (2010) · Zbl 1236.68145 |
| [103] | Péchoux, R, Synthesis of sup-interpretations: a survey, Theoret. Comput. Sci., 467, 30-52, (2013) · Zbl 1282.68091 · doi:10.1016/j.tcs.2012.11.003 |
| [104] | Podelski, A., Rybalchenko, A.: Transition invariants. In: IEEE Computer Society Proceedings of LICS’04, pp. 32-41 (2004) · Zbl 1315.68104 |
| [105] | Prestel, A., Delzell, C.N.: Positive Polynomials. From Hilbert’s 17th Problem to Real Algebra. Springer, Berlin (2001) · Zbl 0987.13016 |
| [106] | Robinson, D.J.S.: A Course in Linear Algebra with Applications, 2nd edn. World Scientific Publishing, Co, Singapore (2006) · Zbl 1114.15003 · doi:10.1142/6237 |
| [107] | Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Proceedings of CAV’13, vol. 8044, pp. 347-363 (2013) |
| [108] | Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Amsterdam (1986) · Zbl 0665.90063 |
| [109] | Schmidt, A, Über deduktive theorien mit mehreren sorten von grunddingen, Matematische Annalen, 115, 485-506, (1938) · JFM 64.0028.01 · doi:10.1007/BF01448954 |
| [110] | Schmidt-Schauss, M.: Computational Aspects Of An Order-Sorted Logic With Term Declarations. PhD Thesis, Fachbereich Informatik der Universität Kaiserslautern (1988) · Zbl 0689.68001 |
| [111] | Shapiro, S.: Foundations without Foundationalism: A Case for Second-Order Logic. Clarendon Press, New York (1991) · Zbl 0732.03002 |
| [112] | Shostak, RE, A practical decision procedure for arithmetic with function symbols, J. ACM, 26, 351-360, (1979) · Zbl 0496.03003 · doi:10.1145/322123.322137 |
| [113] | Smullyan, R.M.: Theory of Formal Systems. Princeton University Press, Princeton (1961) · Zbl 0097.24503 |
| [114] | Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951) · Zbl 0044.25102 |
| [115] | Toyama, Y, Counterexamples to termination for the direct sum of term rewriting systems, Inform. Process. Lett., 25, 141-143, (1987) · Zbl 0653.68010 · doi:10.1016/0020-0190(87)90122-0 |
| [116] | Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, University Mathematics Laboratory, Cambridge, pp. 67-69 (1949) |
| [117] | Urban, C.: The abstract domain of segmented ranking functions. In: Proceeding of SAS’13. LNCS, vol. 7935, pp. 43-62 (2013) · Zbl 1379.68093 |
| [118] | Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Proceedings of TACAS’16. LNCS, vol. 9636, pp. 54-70 (2016) |
| [119] | Waldmann, J.: Matrix interpretations on polyhedral domains. In: Proceedings of RTA’15. LIPICS, vol. 26, pp. 318-333 (2015) · Zbl 1366.68129 |
| [120] | Waldmann, J., Bau, A., Noeth, E.: Matchbox termination prover. http://github.com/jwaldmann/matchbox/ (2014) |
| [121] | Walther, C, A mechanical solution of schubert’s steamroller by many-sorted resolution, Aritif. Intell., 26, 217-224, (1985) · Zbl 0569.68076 · doi:10.1016/0004-3702(85)90029-3 |
| [122] | Wang, H, Logic of many-sorted theories, J. Symb. Logic, 17, 105-116, (1952) · Zbl 0049.14802 · doi:10.2307/2266241 |
| [123] | Zantema, H, Termination of term rewriting: interpretation and type elimination, J. Symb. Comput., 17, 23-50, (1994) · Zbl 0810.68087 · doi:10.1006/jsco.1994.1003 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
