Semantisches Browsen
Aus International Center for Computational Logic
In this chapter, we first motivate equatio … In this chapter, we first motivate equational unification by its applications in theorem proving and term rewriting. In addition to applications that require the computation of unifiers, we will also mention constraint-based approaches, in which only solvability of unification problems (i.e., the existence of unifiers) must be tested. Then we extend the definitions known from syntactic unification (such as most general unifier) to the case of equational unification. It turns out that, for equational unification, one must be more careful when introducing these notions. In the third section, we will mention some unification results for specific equational theories. In the fourth, and central, section of this chapter, we treat the important problem of how to combine unification algorithms. This problem occurs, for example, if we have a unification algorithm that can treat the commutative symbol ``+'' and another algorithm that can treat the associative symbol ``x'', and we want to unify terms that contain both symbols. Finally, we conclude with a short section in which other interesting topics in the field of equational unification are mentioned, which could not be treated in more detail in this chapter.be treated in more detail in this chapter. +
Franz Baader + und K.U. Schulz +
@incollection{ Baader-Schulz-ADHandbook98,
address = {Dordrecht, NL},
author = {F. {Baader} and K.U. {Schulz}},
booktitle = {Automated Deduction -- A Basis for Applications, Vol.~I: Foundations -- Calculi and Methods},
editor = {W. {Bibel} and P.H. {Schmidt}},
pages = {225--263},
publisher = {Kluwer Academic Publishers},
series = {Applied Logic Series},
title = {Unification Theory},
volume = {8},
year = {1998},
}
address = {Dordrecht, NL},
author = {F. {Baader} and K.U. {Schulz}},
booktitle = {Automated Deduction -- A Basis for Applications, Vol.~I: Foundations -- Calculi and Methods},
editor = {W. {Bibel} and P.H. {Schmidt}},
pages = {225--263},
publisher = {Kluwer Academic Publishers},
series = {Applied Logic Series},
title = {Unification Theory},
volume = {8},
year = {1998},
}
Automated Deduction – A Basis for Applications, Vol. I: Foundations – Calculi and Methods +
Baader +
Franz +
Franz Baader, K.U. Schulz<br /> '''[ … Franz Baader, K.U. Schulz<br /> '''[[LATPub140|Unification Theory]]''' <br>__NOTOC__In W. Bibel and P.H. Schmidt, eds., ''Automated Deduction – A Basis for Applications, Vol. I: Foundations – Calculi and Methods'', volume 8 of Applied Logic Series, 225-263. Kluwer Academic Publishers, 1998<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[LATPub140|Details]]tails]] +
Franz Baader, K.U. Schulz<br /> '''[ … Franz Baader, K.U. Schulz<br /> '''[[LATPub140/en|Unification Theory]]''' <br>__NOTOC__In W. Bibel and P.H. Schmidt, eds., ''Automated Deduction – A Basis for Applications, Vol. I: Foundations – Calculi and Methods'', volume 8 of Applied Logic Series, 225-263. Kluwer Academic Publishers, 1998<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[LATPub140|Details]]tails]] +
Anzeigetitel„Anzeigetitel <span style="font-size:small;">(Display title of)</span>“ ist ein softwareseitig fest definiertes Attribut, das einen eindeutigen Anzeigetitel zu einem Objekt speichert und ihm zuweist. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
Unification Theory +
Zuletzt geändert„Zuletzt geändert <span style="font-size:small;">(Modification date)</span>“ ist ein softwareseitig fest definiertes Attribut, das das Datum der letzten Änderung einer Seite speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
25. März 2015, 14:34:02 +
Hat Abfrage„Hat Abfrage <span style="font-size:small;">(Has query)</span>“ ist ein softwareseitig fest definiertes Attribut, das die Metainformationen einer Abfrage als <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Subobject">Subobjekt</a> speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
