Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Inhabitants of Intuitionistic Implicational Theorems Read chapter Read first chapter

2018 | OriginalPaper | Chapter

Symbolic Reasoning Methods in Rewriting Logic and Maude

Author : José Meseguer

Published in: Logic, Language, Information, and Computation

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Rewriting logic is both a logical framework where many logics can be naturally represented, and a semantic framework where many computational systems and programming languages, including concurrent ones, can be both specified and executed. Maude is a declarative specification and programming language based on rewriting logic. For reasoning about the logics and systems represented in the rewriting logic framework symbolic methods are of great importance. This paper discusses various symbolic methods that address crucial reasoning needs in rewriting logic, how they are supported by Maude and other symbolic engines, and various applications that these methods and engines make possible. Because of the generality of rewriting logic, these methods are widely applicable: they can be used in many areas and can provide useful reasoning components for other reasoning engines.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Inhabitants of Intuitionistic Implicational Theorems
next chapter A Semantical View of Proof Systems
Footnotes
1
For a very general formulation of convergence, including conditional equations E, see [84].
 
2
In some cases, the algebra of constructors may have the more general form \(T_{\varOmega /E_{\varOmega } \uplus B_{\varOmega }}\). For example, the data elements may be sets, which, together with axioms \(B_{\varOmega }\) of associativity and commutativity (AC) of set union, may also have an idempotency equation in \(E_{\varOmega }\) which is applied modulo AC to put all set expressions in normal form. All I say applies also to this more general case, but tree automata and/or pattern methods may be more complex in the presence of both axioms and equations for constructors.
 
3
The same remarks as in Footnote 2 apply here: the signature of constructors could more generally be a convergent theory of the form \((\varOmega , E_{\varOmega } \uplus B_{\varOmega })\). Unification modulo \(E_{\varOmega }\uplus B_{\varOmega }\) can still be performed in practice to intersect constrained patterns because in many cases \((\varOmega , E_{\varOmega } \uplus B_{\varOmega })\) has the finite variant property (see Sect. 2.2).
 
4
To avoid wasteful computations we can further make the binary operator \(\wedge \) frozen in its second argument, which forbids rewriting under that second argument. See [95] for a detailed explanation of frozen arguments and [29] for its use in narrowing.
 
5
Here “standard” should be taken with a grain of salt, since extra variables with sorts in \(\varSigma _{0}\) are allowed in the rule’s righthand side v. These extra variables will be mapped by \(\theta \) to new, fresh variables.
 
6
The notation \(\{A\} \mathcal {R} \{B\}\), and the relation to Hoare logic are explained in [125].
 
Literature
1.
2.
Alpuente, M., Escobar, S., Espert, J., Meseguer, J.: A modular order-sorted equational generalization algorithm. Inf. Comput. 235, 98–136 (2014)MathSciNetCrossRef
3.
Alpuente, M., Escobar, S., Iborra, J.: Termination of narrowing revisited. Theor. Comput. Sci. 410(46), 4608–4625 (2009)MathSciNetCrossRef
4.
Alpuente, M., Escobar, S., Iborra, J.: Modular termination of basic narrowing and equational unification. Log. J. IGPL 19(6), 731–762 (2011)MathSciNetCrossRef
5.
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 4:1–4:51 (2009)MathSciNetCrossRef
6.
7.
Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140–164 (2003)MathSciNetCrossRef
8.
Arusoaie, A., Lucanu, D., Rusu, V.: Symbolic execution based on language transformation. Comput. Lang. Syst. Struct. 44, 48–71 (2015)MATH
9.
10.
Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning. Elsevier (1999)CrossRef
11.
Baader, F., Siekmann, J.H.: Unification theory. In: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, pp. 41–126. Oxford University Press (1994)
12.
Bae, K.: Rewriting-based model checking methods. Ph.D. thesis, University of Illinois at Urbana-Champaign (2014)
13.
Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: Rewriting Techniques and Applications (RTA 2013). LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2013)
14.
15.
16.
Bae, K., Meseguer, J.: Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99, 193–234 (2015)CrossRef
17.
18.
19.
Basin, D., Clavel, M., Meseguer, J.: Rewriting logic as a metalogical framework. ACM Trans. Comput. Log. 5, 528–576 (2004)MathSciNetCrossRef
20.
Basin, D., Dreier, J., Sasse, R.: Automated symbolic proofs of observational equivalence. In: Ray, I., Li, N., Kruegel, C. (eds.) Proceedings of the 2015 ACM SIGSAC Conference on Computer and Communications Security, pp. 1144–1155. ACM (2015)
21.
22.
Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial \(\cal{T}\)-satisfiability procedures. J. Log. Comput. 18(1), 77–96 (2008)MathSciNetCrossRef
23.
Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.E.: ELAN from a rewriting logic point of view. Theor. Comput. Sci. 285, 155–185 (2002)MathSciNetCrossRef
24.
Boyer, R., Moore, J.: A Computational Logic. Academic Press, Cambridge (1980)MATH
25.
Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1–3), 386–414 (2006)MathSciNetCrossRef
26.
27.
28.
29.
Cholewa, A., Escobar, S., Meseguer, J.: Constrained narrowing for conditional equational theories modulo axioms. Sci. Comput. Program. 112, 24–57 (2015)CrossRef
30.
31.
32.
33.
Cohn, A.G.: Taxonomic reasoning with many-sorted logics. Artif. Intell. Rev. 3(2–3), 89–128 (1989)
34.
35.
36.
37.
van Deursen, A., Heering, J., Klint, P.: Language Prototyping: An Algebraic Specification Approach. World Scientific, Singapore (1996)CrossRef
38.
39.
Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R.: Automated unbounded verification of stateful cryptographic protocols with exclusive OR. In: Accepted at Computer Security Foundations (CSF) (2018)
40.
Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Adding decision procedures to SMT solvers using axioms with triggers. J. Autom. Reason. 56(4), 387–457 (2016)MathSciNetCrossRef
41.
Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J., Talcott, C.: Associative unification and symbolic reasoning modulo associativity in Maude. In: Preproceedings of WRLA 2018, Thessaloniki, Greece, April 2018. (Distributed in Electronic Form by the ETAPS 2018 Organizers). Proceedings version to appear in LNCS
42.
Durán, F., Meseguer, J., Rocha, C.: Proving ground confluence of equational specifications modulo axioms. Technical report, CS Dept., University of Illinois at Urbana-Champaign, March 2018. http://​hdl.​handle.​net/​2142/​99548. Shorter version to appear in Proceedings of the WRLA 2018. Springer LNCS
43.
Durán, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Algebraic Log. Program. 81, 816–850 (2012)MathSciNetCrossRef
44.
Echenim, M., Peltier, N.: An instantiation scheme for satisfiability modulo theories. J. Autom. Reason. 48(3), 293–362 (2012)MathSciNetCrossRef
45.
Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C.A., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: Asymmetric unification: a new unification paradigm for cryptographic protocol analysis. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 231–248. Springer, Heidelberg (2013). https://​doi.​org/​10.​1007/​978-3-642-38574-2_​16CrossRef
46.
47.
48.
Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: State space reduction in the Maude-NRL protocol analyzer. Inf. Comput. 238, 157–186 (2014)MathSciNetCrossRef
49.
50.
Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Algebraic Log. Program. 81, 898–928 (2012)MathSciNetCrossRef
51.
52.
Fay, M.: First-order unification in an equational theory. In: Proceedings of the 4th Workshop on Automated Deduction, pp. 161–167 (1979)
53.
54.
55.
Frisch, A.M.: The substitutional framework for sorted deduction: fundamental results on hybrid reasoning. Artif. Intell. 49(1–3), 161–198 (1991)MathSciNetCrossRef
56.
Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, Singapore (1998)MATH
57.
Gallagher, J.P.: Tutorial on specialisation of logic programs. In: Proceedings of the 1993 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 1993, pp. 88–98. ACM, New York (1993)
58.
Gallier, J.H., Snyder, W.: Complete sets of transformations for general E-unification. Theor. Comput. Sci. 67(2&3), 203–260 (1989)MathSciNetCrossRef
59.
Garavel, H., Tabikh, M.A., Arrada, I.S.: Benchmarking implementations of term rewriting and pattern matching in algebraic, functional, and object-oriented languages. In: Preproceedings of WRLA 2018, Thessaloniki, Greece, April 2018. (Distributed in electronic form by the ETAPS 2018 Organizers). Proceedings version to appear in LNCS
60.
Goguen, J., Meseguer, J.: Equality, types, modules and (why not?) generics for logic programming. J. Log. Program. 1(2), 179–210 (1984)MathSciNetCrossRef
61.
Goguen, J., Meseguer, J.: Unifying functional, object-oriented and relational programming with logical semantics. In: Shriver, B., Wegner, P. (eds.) Research Directions in Object-Oriented Programming, pp. 417–477. MIT Press, Cambridge (1987)
62.
Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105, 217–273 (1992)MathSciNetCrossRef
63.
Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ: Algebraic Specification in Action, pp. 3–167. Kluwer, Dordrecht (2000)CrossRef
64.
65.
66.
Gutiérrez, R., Meseguer, J.: Variant-based decidable satisfiability in initial algebras with predicates. To appear in Proceedings of LOPSTR 2017. Springer LNCS 2018
67.
68.
Haxthausen, A.E.: Order-sorted algebraic specifications with higher-order functions. Theor. Comput. Sci. 183(2), 157–185 (1997)MathSciNetCrossRef
69.
70.
Hendrix, J., Meseguer, J.: Order-sorted equational unification revisited. Electr. Notes Theor. Comput. Sci. 290, 37–50 (2012)CrossRef
71.
72.
73.
74.
75.
Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15, 1155–1194 (1986)MathSciNetCrossRef
76.
Katelman, M., Keller, S., Meseguer, J.: Rewriting semantics of production rule sets. J. Log. Algebraic Program. 81(7–8), 929–956 (2012)MathSciNetCrossRef
77.
Kirchner, C.: Order-sorted equational unification. Technical report 954, INRIA Lorraine & LORIA, Nancy, France (1988)
78.
79.
Kitzelmann, E., Schmid, U.: Inductive synthesis of functional programs: an explanation based generalization approach. J. Mach. Learn. Res. 7, 429–454 (2006)MathSciNetMATH
80.
Kutsia, T., Levy, J., Villaret, M.: Anti-unification for unranked terms and hedges. In: Schmidt-Schauß, M. (ed.) Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011. LIPIcs, Novi Sad, Serbia, 30 May–1 June 2011, vol. 10, pp. 219–234. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)
81.
Lassez, J.L., Marriott, K.: Explicit representation of terms defined by counter examples. J. Autom. Reason. 3(3), 301–317 (1987)CrossRef
82.
Lu, J., Mylopoulos, J., Harao, M., Hagiya, M.: Higher order generalization and its application in program verification. Ann. Math. Artif. Intell. 28(1–4), 107–126 (2000)MathSciNetCrossRef
83.
84.
Lucas, S., Meseguer, J.: Normal forms and normal theories in conditional rewriting. J. Log. Algebric Methods Program. 85(1), 67–97 (2016)MathSciNetCrossRef
85.
Lynch, C., Morawska, B.: Automatic decidability. In: Proceedings of the LICS 2002, p. 7. IEEE Computer Society (2002)
86.
87.
88.
Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn, pp. 1–87. Kluwer Academic Publishers, Dordrecht (2002). First published as SRI Technical report SRI-CSL-93-05, August 1993MATH
89.
90.
91.
92.
Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. J. High.-Order Symb. Comput. 20(1–2), 123–160 (2007)CrossRef
93.
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)MathSciNetCrossRef
94.
95.
96.
97.
Meseguer, J.: Generalized rewrite theories and coherence completion. Technical report, University of Illinois Computer Science Department, March 2018. http://​hdl.​handle.​net/​2142/​99546. Shorter version to appear in Proceedings of WRLA 2018, Springer LNCS
98.
Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3–41 (2018)CrossRef
99.
100.
101.
Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. Formal Asp. Comput. 29(3), 423–452 (2017)MathSciNetCrossRef
102.
Mogensen, T.Æ.: Glossary for partial evaluation and related topics. High.-Order Symbol. Comput. 13(4), 355–368 (2000)CrossRef
103.
104.
de Moura, L., Rueß, H.: Lemmas on demand for satisfiability solvers. In: Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002), May 2002
105.
Muggleton, S.: Inductive logic programming: issues, results and the challenge of learning language in logic. Artif. Intell. 114(1–2), 283–296 (1999)CrossRef
106.
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)CrossRef
107.
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)MathSciNetCrossRef
108.
Pfenning, F.: Unification and anti-unification in the calculus of constructions. In: Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, 15–18 July 1991, pp. 74–85. IEEE Computer Society (1991)
109.
Plotkin, G.: A note on inductive generalization. In: Machine Intelligence, vol. 5, pp. 153–163. Edinburgh University Press (1970)
110.
Popplestone, R.: An experiment in automatic induction. In: Machine Intelligence, vol. 5, pp. 203–215. Edinburgh University Press (1969)
111.
Reynolds, J.: Transformational systems and the algebraic structure of atomic formulas. Mach. Intell. 5, 135–151 (1970)MathSciNetMATH
112.
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 12, 23–41 (1965)MathSciNetCrossRef
113.
114.
Rocha, C.: Symbolic reachability analysis for rewrite theories. Ph.D. thesis, University of Illinois at Urbana-Champaign (2012)
115.
Rocha, C., Meseguer, J.: Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 603–629. Springer, Heidelberg (2014). https://​doi.​org/​10.​1007/​978-3-642-54624-2_​30CrossRef
116.
Rocha, C., Meseguer, J., Muñoz, C.A.: Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. 86, 269–297 (2017)MathSciNetCrossRef
117.
Rosu, G., Serbanuta, T.: An overview of the K semantic framework. J. Log. Algebraic Program. 79(6), 397–434 (2010)MathSciNetCrossRef
118.
Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Proceedings of the CSF 2012, pp. 78–94. IEEE (2012)
119.
Schmidt, B., Sasse, R., Cremers, C., Basin, D.: Automated verification of group key agreement protocols. In: Proceedings of the 2014 IEEE Symposium on Security and Privacy, SP 2014, pp. 179–194. IEEE Computer Society, Washington, D.C. (2014)
120.
121.
122.
123.
124.
Skeirik, S., Meseguer, J.: Metalevel algorithms for variant satisfiability. J. Log. Algebric Methods Program. 96, 81–110 (2018)MathSciNetCrossRef
125.
Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. Technical report, University of Illinois Computer Science Department, March 2017. http://​hdl.​handle.​net/​2142/​95770. Shorter version to appear in Proceedings of LOPSTR 2107, Springer LNCS 2018
126.
Slagle, J.R.: Automated theorem-proving for theories with simplifiers commutativity, and associativity. J. ACM 21(4), 622–642 (1974)MathSciNetCrossRef
127.
Smolka, G., Aït-Kaci, H.: Inheritance hierarchies: semantics and unification. J. Symb. Comput. 7(3/4), 343–370 (1989)MathSciNetCrossRef
128.
Smolka, G., Nutt, W., Goguen, J., Meseguer, J.: Order-sorted equational computation. In: Nivat, M., Aït-Kaci, H. (eds.) Resolution of Equations in Algebraic Structures, vol. 2, pp. 297–367. Academic Press, Cambridge (1989)
129.
Snyder, W.: A Proof Theory for General Unification. Birkhäuser, Boston (1991)CrossRef
130.
131.
Stefanescu, A., Park, D., Yuwen, S., Li, Y., Rosu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the OOPSLA 2016, pp. 74–91. ACM (2016)
132.
Stehr, M.O.: CINNI - a generic calculus of explicit substitutions and its application to \(\lambda \)-, \(\sigma \)- and \(\pi \)-calculi. ENTCS 36, 70–92 (2000). Proceedings of the 3rd International Workshop on Rewriting Logic and Its ApplicationsMathSciNet
133.
Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 334–375. Springer, Heidelberg (2004). https://​doi.​org/​10.​1007/​978-3-540-39993-3_​16CrossRef
134.
135.
Tushkanova, E., Giorgetti, A., Ringeissen, C., Kouchnarenko, O.: A rule-based system for automatic decidability and combinability. Sci. Comput. Program. 99, 3–23 (2015)CrossRef
136.
137.
Walther, C.: A mechanical solution of Schubert’s steamroller by many-sorted resolution. Artif. Intell. 26(2), 217–224 (1985)MathSciNetCrossRef
138.
Yang, F., Escobar, S., Meadows, C., Meseguer, J., Narendran, P.: Theories of homomorphic encryption, unification, and the finite variant property. In: Proceedings of the PPDP 2014, pp. 123–133. ACM (2014)
139.
Yang, F., Escobar, S., Meadows, C.A., Meseguer, J., Santiago, S.: Strand spaces with choice via a process algebra semantics. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP), Edinburgh, United Kingdom, 5–7 September 2016, pp. 76–89. ACM (2016)
Metadata
Title
Symbolic Reasoning Methods in Rewriting Logic and Maude
Author
José Meseguer
Copyright Year
2018
Publisher
Springer Berlin Heidelberg
Book
Logic, Language, Information, and Computation

Print ISBN: 978-3-662-57668-7

Electronic ISBN: 978-3-662-57669-4

Copyright Year: 2018

DOI
https://doi.org/10.1007/978-3-662-57669-4_2

Premium Partner

    Image Credits