A modular equational generalization algorithm

María Alpuente, Santiago Escobar, José Meseguer, Pedro Ojeda

Research output: Contribution to journalConference article

Abstract

This paper presents a modular equational generalization algorithm, where function symbols can have any combination of associativity, commutativity, and identity axioms (including the empty set). This is suitable for dealing with functions that obey algebraic laws, and are typically mechanized by means of equational atributes in rule-based languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude. The algorithm computes a complete set of least general generalizations modulo the given equational axioms, and is specified by a set of inference rules that we prove correct. This work provides a missing connection between least general generalization and computing modulo equational theories, and opens up new applications of generalization to rule-based languages, theorem provers and program manipulation tools such as partial evaluators, test case generators, and machine learning techniques, where function symbols obey algebraic axioms. A Web tool which implements the algorithm has been developed which is publicly available.

Original languageEnglish (US)
Pages (from-to)24-39
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5438 LNCS
DOIs
StatePublished - Apr 6 2009
Event18th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2008 - Valencia, Spain
Duration: Jul 17 2008Jul 18 2008

Fingerprint

Axioms
Modulo
Maude
Equational Theory
Null set or empty set
Associativity
Learning systems
Inference Rules
Commutativity
Manipulation
Machine Learning
Generator
Partial
Generalization
Computing
Theorem
Language

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

A modular equational generalization algorithm. / Alpuente, María; Escobar, Santiago; Meseguer, José; Ojeda, Pedro.

In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 5438 LNCS, 06.04.2009, p. 24-39.

Research output: Contribution to journalConference article

@article{9db9310eb0cb4f7fbcedd43e0108570b,
title = "A modular equational generalization algorithm",
abstract = "This paper presents a modular equational generalization algorithm, where function symbols can have any combination of associativity, commutativity, and identity axioms (including the empty set). This is suitable for dealing with functions that obey algebraic laws, and are typically mechanized by means of equational atributes in rule-based languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude. The algorithm computes a complete set of least general generalizations modulo the given equational axioms, and is specified by a set of inference rules that we prove correct. This work provides a missing connection between least general generalization and computing modulo equational theories, and opens up new applications of generalization to rule-based languages, theorem provers and program manipulation tools such as partial evaluators, test case generators, and machine learning techniques, where function symbols obey algebraic axioms. A Web tool which implements the algorithm has been developed which is publicly available.",
author = "Mar{\'i}a Alpuente and Santiago Escobar and Jos{\'e} Meseguer and Pedro Ojeda",
year = "2009",
month = "4",
day = "6",
doi = "10.1007/978-3-642-00515-2_3",
language = "English (US)",
volume = "5438 LNCS",
pages = "24--39",
journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - A modular equational generalization algorithm

AU - Alpuente, María

AU - Escobar, Santiago

AU - Meseguer, José

AU - Ojeda, Pedro

PY - 2009/4/6

Y1 - 2009/4/6

N2 - This paper presents a modular equational generalization algorithm, where function symbols can have any combination of associativity, commutativity, and identity axioms (including the empty set). This is suitable for dealing with functions that obey algebraic laws, and are typically mechanized by means of equational atributes in rule-based languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude. The algorithm computes a complete set of least general generalizations modulo the given equational axioms, and is specified by a set of inference rules that we prove correct. This work provides a missing connection between least general generalization and computing modulo equational theories, and opens up new applications of generalization to rule-based languages, theorem provers and program manipulation tools such as partial evaluators, test case generators, and machine learning techniques, where function symbols obey algebraic axioms. A Web tool which implements the algorithm has been developed which is publicly available.

AB - This paper presents a modular equational generalization algorithm, where function symbols can have any combination of associativity, commutativity, and identity axioms (including the empty set). This is suitable for dealing with functions that obey algebraic laws, and are typically mechanized by means of equational atributes in rule-based languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude. The algorithm computes a complete set of least general generalizations modulo the given equational axioms, and is specified by a set of inference rules that we prove correct. This work provides a missing connection between least general generalization and computing modulo equational theories, and opens up new applications of generalization to rule-based languages, theorem provers and program manipulation tools such as partial evaluators, test case generators, and machine learning techniques, where function symbols obey algebraic axioms. A Web tool which implements the algorithm has been developed which is publicly available.

UR - http://www.scopus.com/inward/record.url?scp=63449094344&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=63449094344&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-00515-2_3

DO - 10.1007/978-3-642-00515-2_3

M3 - Conference article

AN - SCOPUS:63449094344

VL - 5438 LNCS

SP - 24

EP - 39

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SN - 0302-9743

ER -