Mostrar el registro sencillo del ítem
dc.contributor.author | Alpuente Frasnedo, María | es_ES |
dc.contributor.author | Escobar Román, Santiago | es_ES |
dc.contributor.author | Meseguer, José | es_ES |
dc.contributor.author | Sapiña-Sanchis, Julia | es_ES |
dc.date.accessioned | 2023-03-23T19:01:47Z | |
dc.date.available | 2023-03-23T19:01:47Z | |
dc.date.issued | 2022-05 | es_ES |
dc.identifier.issn | 1012-2443 | es_ES |
dc.identifier.uri | http://hdl.handle.net/10251/192568 | |
dc.description.abstract | [EN] Generalization, also called anti-unification, is the dual of unification. A generalizer of two terms t and t' is a term t '' of which t and t' are substitution instances. The dual of most general equational unifiers is that of least general equational generalizers, i.e., most specific anti-instances modulo equations. In a previous work, we extended the classical untyped generalization algorithm to: (1) an order-sorted typed setting with sorts, subsorts, and subtype polymorphism; (2) work modulo equational theories, where function symbols can obey any combination of associativity, commutativity, and identity axioms (including the empty set of such axioms); and (3) the combination of both, which results in a modular, order-sorted equational generalization algorithm. However, Cerna and Kutsia showed that our algorithm is generally incomplete for the case of identity axioms and a counterexample was given. Furthermore, they proved that, in theories with two identity elements or more, generalization with identity axioms is generally nullary, yet it is finitary for both the linear and one-unital fragments, i.e., either solutions with repeated variables are disregarded or the considered theories are restricted to having just one function symbol with an identity or unit element. In this work, we show how we can easily extend our original inference system to cope with the non-linear fragment and identify a more general class than one-unit theories where generalization with identity axioms is finitary. | es_ES |
dc.language | Inglés | es_ES |
dc.publisher | Springer-Verlag | es_ES |
dc.relation.ispartof | Annals of Mathematics and Artificial Intelligence | es_ES |
dc.rights | Reserva de todos los derechos | es_ES |
dc.subject | Least general generalization | es_ES |
dc.subject | Rule-based languages | es_ES |
dc.subject | Equational reasoning | es_ES |
dc.subject | Order-Sorted | es_ES |
dc.subject | Associativity | es_ES |
dc.subject | Commutativity | es_ES |
dc.subject | Identity | es_ES |
dc.subject.classification | LENGUAJES Y SISTEMAS INFORMATICOS | es_ES |
dc.title | Order-sorted Equational Generalization Algorithm Revisited | es_ES |
dc.type | Artículo | es_ES |
dc.identifier.doi | 10.1007/s10472-021-09771-1 | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C32/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/GENERALITAT VALENCIANA//PROMETEO%2F2019%2F098//DEEPTRUST/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/EC/H2020/952215/EU | es_ES |
dc.rights.accessRights | Abierto | es_ES |
dc.contributor.affiliation | Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica | es_ES |
dc.description.bibliographicCitation | Alpuente Frasnedo, M.; Escobar Román, S.; Meseguer, J.; Sapiña-Sanchis, J. (2022). Order-sorted Equational Generalization Algorithm Revisited. Annals of Mathematics and Artificial Intelligence. 90(5):499-522. https://doi.org/10.1007/s10472-021-09771-1 | es_ES |
dc.description.accrualMethod | S | es_ES |
dc.relation.publisherversion | https://doi.org/10.1007/s10472-021-09771-1 | es_ES |
dc.description.upvformatpinicio | 499 | es_ES |
dc.description.upvformatpfin | 522 | es_ES |
dc.type.version | info:eu-repo/semantics/publishedVersion | es_ES |
dc.description.volume | 90 | es_ES |
dc.description.issue | 5 | es_ES |
dc.relation.pasarela | S\446554 | es_ES |
dc.contributor.funder | GENERALITAT VALENCIANA | es_ES |
dc.contributor.funder | AGENCIA ESTATAL DE INVESTIGACION | es_ES |
dc.contributor.funder | COMISION DE LAS COMUNIDADES EUROPEA | es_ES |
dc.description.references | Alpuente, M., Escobar, S., Meseguer, J., Ojeda, P.: A modular equational generalization algorithm. In: Hanus, M. (ed.) Logic-based program synthesis and transformation, 18th international symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers, Springer, Lecture Notes in Computer Science, vol. 5438, pp 24–39 (2008), https://doi.org/10.1007/978-3-642-00515-2_3 | es_ES |
dc.description.references | Alpuente, M., Escobar, S., Meseguer, J., Ojeda, P.: Order-sorted generalization. Electr Notes Theor Comput Sci 246, 27–38 (2009). https://doi.org/10.1016/j.entcs.2009.07.013 | es_ES |
dc.description.references | Alpuente, M., Escobar, S., Espert, J., Meseguer, J.: ACUOS: A system for modular ACU generalization with subtyping and inheritance. In: Proceedings of the 14th European Conference on Logics in Artificial Intelligence (JELIA 2014), Springer-Verlag, Berlin, Lecture Notes in Computer Science, vol. 8761, pp 573–581 (2014) | es_ES |
dc.description.references | Alpuente, M., Escobar, S., Espert, J., Meseguer, J.: A modular order-sorted equational generalization algorithm. Inf. Comput. 235, 98–136 (2014). https://doi.org/10.1016/j.ic.2014.01.006 | es_ES |
dc.description.references | Alpuente, M., Ballis, D., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: ACUOS2: a high-performance system for modular ACU generalization with subtyping and inheritance. In: Proceedings of the 16th European Conference on Logics in Artificial Intelligence (JELIA 2019), Springer-Verlag, Berlin, Lecture Notes in Computer Science, vol. 11468, pp 171–181 (2019) | es_ES |
dc.description.references | Alpuente, M., Ballis, D., Sapiña, J.: Efficient safety enforcement for Maude programs via program specialization in the ÁTAME system. Math. Comput. Sci. 14(3), 591–606 (2020) | es_ES |
dc.description.references | Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: A partial evaluation framework for order-sorted equational programs modulo axioms. 110: 1–36 (2020) | es_ES |
dc.description.references | Armengol, E.: Usages of generalization in case-based reasoning. In: Proceedings of the 7th International Conference on Case-Based Reasoning (ICCBR 2007), Springer-Verlag, Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-540-74141-1_3, vol. 4626, pp 31–45 (2007) | es_ES |
dc.description.references | Baumgartner, A., Kutsia, T., Levy, J., Villaret, M.: Term-graph anti-unification. In: FSCD, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, LIPIcs, vol. 108, pp 9:1–9:17 (2018) | es_ES |
dc.description.references | Cerna, D.M., Kutsia, T.: Unital anti-unification: Type and algorithms. In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs, vol. 167, pp 26:1–26:20 (2020), https://doi.org/10.4230/LIPIcs.FSCD.2020.26 | es_ES |
dc.description.references | Durán, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCos, Springer, Lecture Notes in Computer Science, vol. 5749, pp 246–262 (2009) | es_ES |
dc.description.references | Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program 81(7-8), 898–928 (2012) | es_ES |
dc.description.references | 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) | es_ES |
dc.description.references | Huet, G.: Resolution d’equations dans des langages d’order 1, 2,…,ω. PhD thesis, Univ, Paris VII (1976) | es_ES |
dc.description.references | Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F (ed.) Proceedings of 12th International Workshop on Recent Trends in Algebraic Development Techniques, WADT’97, Springer, LNCS, vol. 1376, pp 18–61 (1997) | es_ES |
dc.description.references | Muggleton, S.: Inductive Logic Programming: Issues, Results and the Challenge of Learning Language in Logic. Artif. Intell. 114(1-2), 283–296 (1999) | es_ES |
dc.description.references | Ontañón, S., Plaza, E.: Similarity measures over refinement graphs. Mach. Learn. 87(1), 57–92 (2012). https://doi.org/10.1007/s10994-011-5274-3 | es_ES |
dc.description.references | Plotkin, G.: A note on inductive generalization. In: Machine Intelligence, vol. 5, pp 153–163. Edinburgh University Press (1970) | es_ES |
dc.description.references | Reynolds, J.: Transformational systems and the algebraic structure of atomic formulas. Mach. Intell. 5, 135–151 (1970) | es_ES |
dc.description.references | TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003) | es_ES |