- Titel
- Approximately Solving Set Equations
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-795831
- Schriftenreihe
- LTCS-Report
- Bandnummer
- 16-03
- Erstveröffentlichung
- 2016
- DOI
- https://doi.org/10.25368/2022.227
- Abstract (EN)
- Unification with constants modulo the theory ACUI of an associative (A), commutative (C) and idempotent (I) binary function symbol with a unit (U) corresponds to solving a very simple type of set equations. It is well-known that solvability of systems of such equations can be decided in polynomial time by reducing it to satisfiability of propositional Horn formulae. Here we introduce a modified version of this problem by no longer requiring all equations to be completely solved, but allowing for a certain number of violations of the equations. We introduce three different ways of counting the number of violations, and investigate the complexity of the respective decision problem, i.e., the problem of deciding whether there is an assignment that solves the system with at most l violations for a given threshold value l.
- Submitted to 30th International Workshop on Unification
- Freie Schlagwörter (DE)
- Vereinheitlichung, Entscheidungsproblem, ACUI
- Freie Schlagwörter (EN)
- unification, decision problem, ACUI
- Klassifikation (DDC)
- 004
- Klassifikation (RVK)
- ST 136
- Publizierende Institution
- Technische Universität Dresden, Dresden
- Version / Begutachtungsstatus
- angenommene Version / Postprint / Autorenversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-795831
- Veröffentlichungsdatum Qucosa
- 20.06.2022
- Dokumenttyp
- Bericht
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0