5 Search Results for "Furbach, Ulrich"

Document
DOI: 10.4230/LIPIcs.FSCD.2025.8
The Unification Type of an Equational Theory May Depend on the Instantiation Preorder

Authors: Franz Baader and Oliver Fernández Gil

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. It has been known for more than three decades that the unification type of an equational theory may vary, depending on which instantiation preorder is used. More precisely, it was shown in 1991 that the theory ACUI of an associative, commutative, and idempotent binary function symbol with a unit is unitary w.r.t. the restricted instantiation preorder, but not unitary w.r.t. the unrestricted one. In 2016 this result was strengthened by showing that the unrestricted type of this theory also cannot be finitary. Here, we considerably improve on this result by proving that ACUI is infinitary w.r.t. the unrestricted instantiation preorder, thus precluding type zero. We also show that, w.r.t. this preorder, the unification type of ACU (where idempotency is removed from the axioms) and of AC (where additionally the unit is removed) is infinitary, though it is respectively unitary and finitary in the restricted case. In the other direction, we prove (using the example of unification in the description logic EL) that the unification type may actually improve from type zero to infinitary when switching from the restricted instantiation preorder to the unrestricted one. In addition, we establish some general results on the relationship between the two instantiation preorders.
Cite as

Franz Baader and Oliver Fernández Gil. The Unification Type of an Equational Theory May Depend on the Instantiation Preorder. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:LIPIcs.FSCD.2025.8,
  author =	{Baader, Franz and Fern\'{a}ndez Gil, Oliver},
  title =	{{The Unification Type of an Equational Theory May Depend on the Instantiation Preorder}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{8:1--8:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.8},
  URN =		{urn:nbn:de:0030-drops-236230},
  doi =		{10.4230/LIPIcs.FSCD.2025.8},
  annote =	{Keywords: Unification type, Instantiation preorder, Equational theories, Modal and Description Logics}
}
Document
DOI: 10.4230/DagSemRep.300
Deduction (Dagstuhl Seminar 01101)

Authors: Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur. Deduction (Dagstuhl Seminar 01101). Dagstuhl Seminar Report 300, pp. 1-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2001)

Copy BibTex To Clipboard

@TechReport{furbach_et_al:DagSemRep.300,
  author =	{Furbach, Ulrich and Ganzinger, Harald and Hasegawa, Ryuzo and Kapur, Deepak},
  title =	{{Deduction (Dagstuhl Seminar 01101)}},
  pages =	{1--27},
  ISSN =	{1619-0203},
  year =	{2001},
  type = 	{Dagstuhl Seminar Report},
  number =	{300},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.300},
  URN =		{urn:nbn:de:0030-drops-151843},
  doi =		{10.4230/DagSemRep.300},
}
Document
DOI: 10.4230/DagSemRep.232
Deduction (Dagstuhl Seminar 99091)

Authors: Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur. Deduction (Dagstuhl Seminar 99091). Dagstuhl Seminar Report 232, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2000)

Copy BibTex To Clipboard

@TechReport{furbach_et_al:DagSemRep.232,
  author =	{Furbach, Ulrich and Ganzinger, Harald and Hasegawa, Ryuzo and Kapur, Deepak},
  title =	{{Deduction (Dagstuhl Seminar 99091)}},
  pages =	{1--24},
  ISSN =	{1619-0203},
  year =	{2000},
  type = 	{Dagstuhl Seminar Report},
  number =	{232},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.232},
  URN =		{urn:nbn:de:0030-drops-151182},
  doi =		{10.4230/DagSemRep.232},
}
Document
DOI: 10.4230/DagSemRep.170
Deduction (Dagstuhl Seminar 9709)

Authors: Wolfgang Bibel, Ulrich Furbach, Ryuzo Hasegawa, and Mark Stickel

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Wolfgang Bibel, Ulrich Furbach, Ryuzo Hasegawa, and Mark Stickel. Deduction (Dagstuhl Seminar 9709). Dagstuhl Seminar Report 170, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1997)

Copy BibTex To Clipboard

@TechReport{bibel_et_al:DagSemRep.170,
  author =	{Bibel, Wolfgang and Furbach, Ulrich and Hasegawa, Ryuzo and Stickel, Mark},
  title =	{{Deduction (Dagstuhl Seminar 9709)}},
  pages =	{1--23},
  ISSN =	{1619-0203},
  year =	{1997},
  type = 	{Dagstuhl Seminar Report},
  number =	{170},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.170},
  URN =		{urn:nbn:de:0030-drops-150577},
  doi =		{10.4230/DagSemRep.170},
}
Document
DOI: 10.4230/DagSemRep.49
Analogical and Inductive Inference 1992 (Dagstuhl Seminar 9241)

Authors: Robert P. Daley, Ulrich Furbach, and Klaus Peter Jantke

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Robert P. Daley, Ulrich Furbach, and Klaus Peter Jantke. Analogical and Inductive Inference 1992 (Dagstuhl Seminar 9241). Dagstuhl Seminar Report 49, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1992)

Copy BibTex To Clipboard

@TechReport{daley_et_al:DagSemRep.49,
  author =	{Daley, Robert P. and Furbach, Ulrich and Jantke, Klaus Peter},
  title =	{{Analogical and Inductive Inference 1992 (Dagstuhl Seminar 9241)}},
  pages =	{1--28},
  ISSN =	{1619-0203},
  year =	{1992},
  type = 	{Dagstuhl Seminar Report},
  number =	{49},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.49},
  URN =		{urn:nbn:de:0030-drops-149374},
  doi =		{10.4230/DagSemRep.49},
}
  • Refine by Type
  • 5 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2001
  • 1 2000
  • 1 1997
  • 1 1992

  • Refine by Author
  • 4 Furbach, Ulrich
  • 3 Hasegawa, Ryuzo
  • 2 Ganzinger, Harald
  • 2 Kapur, Deepak
  • 1 Baader, Franz
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 4 DagSemRep

  • Refine by Classification
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Description logics
  • 1 Theory of computation → Equational logic and rewriting

  • Refine by Keyword
  • 1 Equational theories
  • 1 Instantiation preorder
  • 1 Modal and Description Logics
  • 1 Unification type

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact