Skolemization and Decidability of the Bernays-Schoenfinkel Class in Goedel Logics

Fuente: arXiv
Enregistré dans:
Détails bibliographiques
Auteurs principaux: Gamsakhurdia, Mariami, Baaz, Matthias, Lolic, Anela
Format: Preprint
Publié: 2025
Sujets:
Accès en ligne:
Tags: Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
_version_ 1866912751717187584
author Gamsakhurdia, Mariami
Baaz, Matthias
Lolic, Anela
author_facet Gamsakhurdia, Mariami
Baaz, Matthias
Lolic, Anela
contents In 1928, Bernays and Schoenfinkel proved the decidability of prenex sentences whose matrices contain no function symbols, now known as the Bernays-Schoenfinkel (BS) class. We investigate the decidability of the BS class for all Goedel logics. Our validity argument relies on the fact that Skolemization works for prenex Goedel logics, while 1-satisfiability follows from structural properties of prenex formulas. We show that validity and 1-satisfiability for the BS class are decidable in every Goedel logic, and that these properties persist across all infinite Goedel logics.
format Preprint
id arxiv_https___arxiv_org_abs_2512_05772
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Skolemization and Decidability of the Bernays-Schoenfinkel Class in Goedel Logics
Gamsakhurdia, Mariami
Baaz, Matthias
Lolic, Anela
Logic in Computer Science
In 1928, Bernays and Schoenfinkel proved the decidability of prenex sentences whose matrices contain no function symbols, now known as the Bernays-Schoenfinkel (BS) class. We investigate the decidability of the BS class for all Goedel logics. Our validity argument relies on the fact that Skolemization works for prenex Goedel logics, while 1-satisfiability follows from structural properties of prenex formulas. We show that validity and 1-satisfiability for the BS class are decidable in every Goedel logic, and that these properties persist across all infinite Goedel logics.
title Skolemization and Decidability of the Bernays-Schoenfinkel Class in Goedel Logics
topic Logic in Computer Science
url https://arxiv.org/abs/2512.05772