LATPub100: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
||
| (2 dazwischenliegende Versionen desselben Benutzers werden nicht angezeigt) | |||
| Zeile 1: | Zeile 1: | ||
{{Publikation Erster Autor | {{Publikation Erster Autor | ||
|ErsterAutorVorname= | |ErsterAutorVorname=Franz | ||
|ErsterAutorNachname=Baader | |ErsterAutorNachname=Baader | ||
|FurtherAuthors=W. Nutt | |FurtherAuthors=W. Nutt | ||
| Zeile 6: | Zeile 6: | ||
{{Article | {{Article | ||
|Referiert=1 | |Referiert=1 | ||
|Title=Combination Problems for Commutative/Monoidal Theories: | |Title=Combination Problems for Commutative/Monoidal Theories: How Algebra Can Help in Equational Reasoning | ||
|Year=1996 | |Year=1996 | ||
|Month= | |Month= | ||
| Zeile 12: | Zeile 12: | ||
|Note= | |Note= | ||
|Number=4 | |Number=4 | ||
|Pages=309 | |Pages=309-337 | ||
|Publisher= | |Publisher= | ||
|Volume=7 | |Volume=7 | ||
| Zeile 18: | Zeile 18: | ||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract= | |Abstract=We study the class of theories for which solving unification problems is equivalent to solving systems of linear equations over a semiring. It encompasses important examples like the theories of Abelian monoids, idempotent Abelian monoids, and Abelian groups. This class has been introduced by the authors independently of each other as ``commutative theories'' (Baader) and ``monoidal theories'' (Nutt). | ||
We show that commutative theories and monoidal theories indeed define the same class (modulo a translation of the signature), and we prove that it is undecidable whether a given theory belongs to it. In the remainder of the paper we investigate combinations of commutative/monoidal theories with other theories. We show that finitary commutative/monoidal theories always satisfy the requirements for applying general methods developed for the combination of unification algorithms for disjoint equational theories. | |||
We study the class of theories for which solving unification | Then we study the adjunction of monoids of homomorphismss to commutative/monoidal theories. This is a special case of a non-disjoint combination, which has an algebraic counterpart in the corresponding semiring. By studying equations over this semiring, we identify a large subclass of commutative/monoidal theories that are of unification type zero by. We also show with methods from linear algebra that unitary and finitary commutative/monoidal theories do not change their unification type when they are augmented by a finite monoid of hom s, and how algorithms for the extended theory can be obtained from algorithms for the basic theory. | ||
problems is equivalent to solving systems of linear equations | |||
over a semiring. It encompasses important examples like the theories of | |||
Abelian monoids, idempotent Abelian monoids, and Abelian groups. | |||
This class has been introduced by the authors independently | |||
of each other as ``commutative theories'' (Baader) | |||
and ``monoidal theories'' (Nutt). | |||
We show that commutative theories and monoidal theories indeed define the same class | |||
(modulo a translation of the signature), and we prove that it is undecidable | |||
whether a given theory belongs to it. | |||
In the remainder of the paper we investigate | |||
combinations of commutative/monoidal theories with other theories. | |||
We show that finitary commutative/monoidal theories always satisfy the | |||
requirements for applying general methods developed for the combination of | |||
unification algorithms for disjoint equational theories. | |||
Then we study the adjunction of monoids of homomorphismss to | |||
commutative/monoidal theories. | |||
This is a special case of a non-disjoint combination, | |||
which has an algebraic counterpart in the corresponding semiring. | |||
By studying equations over this semiring, | |||
we identify a large subclass of commutative/monoidal theories | |||
that are of unification type zero by. | |||
We also show with methods from linear algebra | |||
that unitary and finitary commutative/monoidal theories | |||
do not change their unification type | |||
when they are augmented by a finite monoid of | |||
and how algorithms for the extended theory can be obtained from | |||
algorithms for the basic theory. | |||
|ISBN= | |ISBN= | ||
|ISSN= | |ISSN= | ||
| Zeile 72: | Zeile 38: | ||
year = {1996}, | year = {1996}, | ||
} | } | ||
}} | }} | ||
Aktuelle Version vom 25. März 2015, 16:34 Uhr
Combination Problems for Commutative/Monoidal Theories: How Algebra Can Help in Equational Reasoning
Franz BaaderFranz Baader, W. NuttW. Nutt
Franz Baader, W. Nutt
Combination Problems for Commutative/Monoidal Theories: How Algebra Can Help in Equational Reasoning
J. Applicable Algebra in Engineering, Communication and Computing, 7(4):309-337, 1996
Combination Problems for Commutative/Monoidal Theories: How Algebra Can Help in Equational Reasoning
J. Applicable Algebra in Engineering, Communication and Computing, 7(4):309-337, 1996
- KurzfassungAbstract
We study the class of theories for which solving unification problems is equivalent to solving systems of linear equations over a semiring. It encompasses important examples like the theories of Abelian monoids, idempotent Abelian monoids, and Abelian groups. This class has been introduced by the authors independently of each other as ``commutative theories (Baader) and ``monoidal theories (Nutt).We show that commutative theories and monoidal theories indeed define the same class (modulo a translation of the signature), and we prove that it is undecidable whether a given theory belongs to it. In the remainder of the paper we investigate combinations of commutative/monoidal theories with other theories. We show that finitary commutative/monoidal theories always satisfy the requirements for applying general methods developed for the combination of unification algorithms for disjoint equational theories.
Then we study the adjunction of monoids of homomorphismss to commutative/monoidal theories. This is a special case of a non-disjoint combination, which has an algebraic counterpart in the corresponding semiring. By studying equations over this semiring, we identify a large subclass of commutative/monoidal theories that are of unification type zero by. We also show with methods from linear algebra that unitary and finitary commutative/monoidal theories do not change their unification type when they are augmented by a finite monoid of hom s, and how algorithms for the extended theory can be obtained from algorithms for the basic theory. - Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@article{ BaaderNutt-AAECC-96,
author = {F. {Baader} and W. {Nutt}},
journal = {J. Applicable Algebra in Engineering, Communication and Computing},
number = {4},
pages = {309--337},
title = {Combination Problems for Commutative/Monoidal Theories: {H}ow Algebra Can Help in Equational Reasoning},
volume = {7},
year = {1996},
}
