Search Results

Documents authored by Dundua, Besik

Document
DOI: 10.4230/LIPIcs.TYPES.2025.7
Towards Fuzzy Constructive Type Theories

Authors: Besik Dundua, Furio Honsell, Temur Kutsia, Marina Lenisa, and Luigi Liquori

Published in: LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025)

Abstract
In this paper, we explore combinations of Fuzzy Logic and Constructive Higher Order Type Theory. Although Fuzzy Logic is more than 60 years old, and Fuzzy Type Theories have been studied in the classical case of Church’s Theory of Types, there is yet no satisfactory understanding of how to deal with judgements of the shape Γ⊢ M:_d A, where d is a fuzzy degree of confidence. Addressing this issue is important in view of the growing interest in quantitative and non-idempotent type theories. To this end, we introduce fuzzy type assignment systems in order to investigate how minimal fuzzy formulæbehave as types, according to some fuzzy proposition-as-types paradigm. Moreover, we study a fuzzy version of intersection types. In both systems assumptions are multisets and d, in Γ⊢ M:_d A, is a formula of minimal propositional Fuzzy Logic. Evaluating d in a residuated lattice [0,1], endowed with a left-continuous T-norm, we can analyse how the degree of confidence propagates from the assumptions to the conclusion, thereby yielding new information on the derivation. The former system sheds light on the connection between minimal Fuzzy Logics and affine λ-calculus and permits to show that the tautologies in the BCK-logic amount to the simple types which are inhabited by BCK-combinators. The latter system keeps track of the number of times a given fuzzy assumption is made. We discuss the standard suite of metatheorems (inversion lemmata and subject-conversion) for the systems, and point to possible uses of the fuzzy formula attached to the membership construct.
Cite as

Besik Dundua, Furio Honsell, Temur Kutsia, Marina Lenisa, and Luigi Liquori. Towards Fuzzy Constructive Type Theories. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dundua_et_al:LIPIcs.TYPES.2025.7,
  author =	{Dundua, Besik and Honsell, Furio and Kutsia, Temur and Lenisa, Marina and Liquori, Luigi},
  title =	{{Towards Fuzzy Constructive Type Theories}},
  booktitle =	{31st International Conference on Types for Proofs and Programs (TYPES 2025)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-441-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{384},
  editor =	{Nordvall Forsberg, Fredrik and McKinna, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.7},
  URN =		{urn:nbn:de:0030-drops-270256},
  doi =		{10.4230/LIPIcs.TYPES.2025.7},
  annote =	{Keywords: Fuzzy type theory, constructive type theory, lambda calculus, residuated lattices}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.30
Constraint Solving over Multiple Similarity Relations

Authors: Besik Dundua, Temur Kutsia, Mircea Marin, and Cleopatra Pau

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Similarity relations are reflexive, symmetric, and transitive fuzzy relations. They help to make approximate inferences, replacing the notion of equality. Similarity-based unification has been quite intensively investigated, as a core computational method for approximate reasoning and declarative programming. In this paper we consider solving constraints over several similarity relations, instead of a single one. Multiple similarities pose challenges to constraint solving, since we can not rely on the transitivity property anymore. Existing methods for unification with fuzzy proximity relations (reflexive, symmetric, non-transitive relations) do not provide a solution that would adequately reflect particularities of dealing with multiple similarities. To address this problem, we develop a constraint solving algorithm for multiple similarity relations, prove its termination, soundness, and completeness properties, and discuss applications.
Cite as

Besik Dundua, Temur Kutsia, Mircea Marin, and Cleopatra Pau. Constraint Solving over Multiple Similarity Relations. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dundua_et_al:LIPIcs.FSCD.2020.30,
  author =	{Dundua, Besik and Kutsia, Temur and Marin, Mircea and Pau, Cleopatra},
  title =	{{Constraint Solving over Multiple Similarity Relations}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{30:1--30:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.30},
  URN =		{urn:nbn:de:0030-drops-123522},
  doi =		{10.4230/LIPIcs.FSCD.2020.30},
  annote =	{Keywords: Fuzzy relations, similarity, constraint solving}
}
Document
DOI: 10.4230/OASIcs.ICLP.2016.10
P-rho-Log: Combining Logic Programming with Conditional Transformation Systems

Authors: Besik Dundua, Temur Kutsia, and Klaus Reisenberger-Hagmayer

Published in: OASIcs, Volume 52, Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)

Abstract
P-rho-Log extends Prolog by conditional transformations that are controlled by strategies. We give a brief overview of the tool and illustrate its capabilities.
Cite as

Besik Dundua, Temur Kutsia, and Klaus Reisenberger-Hagmayer. P-rho-Log: Combining Logic Programming with Conditional Transformation Systems. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016). Open Access Series in Informatics (OASIcs), Volume 52, pp. 10:1-10:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dundua_et_al:OASIcs.ICLP.2016.10,
  author =	{Dundua, Besik and Kutsia, Temur and Reisenberger-Hagmayer, Klaus},
  title =	{{P-rho-Log: Combining Logic Programming with Conditional Transformation Systems}},
  booktitle =	{Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)},
  pages =	{10:1--10:5},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-007-1},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{52},
  editor =	{Carro, Manuel and King, Andy and Saeedloei, Neda and De Vos, Marina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2016.10},
  URN =		{urn:nbn:de:0030-drops-67409},
  doi =		{10.4230/OASIcs.ICLP.2016.10},
  annote =	{Keywords: Conditional transformation rules, strategies, Prolog}
}
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