Admissibility in Finitely Generated Quasivarieties
Checking the admissibility of quasiequations in a finitely generated (i.e., generated by a finite set of finite algebras) quasivariety Q amounts to checking validity in a suitable finite free algebra of the quasivariety, and is therefore decidable. However, since free algebras may be large even for...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2013-06-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/733/pdf |
| _version_ | 1827322843445067776 |
|---|---|
| author | George Metcalfe Christoph Röthlisberger |
| author_facet | George Metcalfe Christoph Röthlisberger |
| author_sort | George Metcalfe |
| collection | DOAJ |
| description | Checking the admissibility of quasiequations in a finitely generated (i.e.,
generated by a finite set of finite algebras) quasivariety Q amounts to
checking validity in a suitable finite free algebra of the quasivariety, and is
therefore decidable. However, since free algebras may be large even for small
sets of small algebras and very few generators, this naive method for checking
admissibility in $\Q$ is not computationally feasible. In this paper,
algorithms are introduced that generate a minimal (with respect to a multiset
well-ordering on their cardinalities) finite set of algebras such that the
validity of a quasiequation in this set corresponds to admissibility of the
quasiequation in Q. In particular, structural completeness (validity and
admissibility coincide) and almost structural completeness (validity and
admissibility coincide for quasiequations with unifiable premises) can be
checked. The algorithms are illustrated with a selection of well-known finitely
generated quasivarieties, and adapted to handle also admissibility of rules in
finite-valued logics. |
| first_indexed | 2024-04-25T01:36:22Z |
| format | Article |
| id | doaj.art-2e2736c5ebc24bf794d564fbaf923f62 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:22Z |
| publishDate | 2013-06-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-2e2736c5ebc24bf794d564fbaf923f622024-03-08T09:30:58ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742013-06-01Volume 9, Issue 210.2168/LMCS-9(2:9)2013733Admissibility in Finitely Generated QuasivarietiesGeorge MetcalfeChristoph RöthlisbergerChecking the admissibility of quasiequations in a finitely generated (i.e., generated by a finite set of finite algebras) quasivariety Q amounts to checking validity in a suitable finite free algebra of the quasivariety, and is therefore decidable. However, since free algebras may be large even for small sets of small algebras and very few generators, this naive method for checking admissibility in $\Q$ is not computationally feasible. In this paper, algorithms are introduced that generate a minimal (with respect to a multiset well-ordering on their cardinalities) finite set of algebras such that the validity of a quasiequation in this set corresponds to admissibility of the quasiequation in Q. In particular, structural completeness (validity and admissibility coincide) and almost structural completeness (validity and admissibility coincide for quasiequations with unifiable premises) can be checked. The algorithms are illustrated with a selection of well-known finitely generated quasivarieties, and adapted to handle also admissibility of rules in finite-valued logics.https://lmcs.episciences.org/733/pdfcomputer science - logic in computer sciencemathematics - logic |
| spellingShingle | George Metcalfe Christoph Röthlisberger Admissibility in Finitely Generated Quasivarieties Logical Methods in Computer Science computer science - logic in computer science mathematics - logic |
| title | Admissibility in Finitely Generated Quasivarieties |
| title_full | Admissibility in Finitely Generated Quasivarieties |
| title_fullStr | Admissibility in Finitely Generated Quasivarieties |
| title_full_unstemmed | Admissibility in Finitely Generated Quasivarieties |
| title_short | Admissibility in Finitely Generated Quasivarieties |
| title_sort | admissibility in finitely generated quasivarieties |
| topic | computer science - logic in computer science mathematics - logic |
| url | https://lmcs.episciences.org/733/pdf |
| work_keys_str_mv | AT georgemetcalfe admissibilityinfinitelygeneratedquasivarieties AT christophrothlisberger admissibilityinfinitelygeneratedquasivarieties |