| German |
| has gloss | deu: Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Für Formeln in Skolemform existiert ein berechenbarer Test auf Erfüllbarkeit. Dies ist nützlich, da jede Formelmenge X genau dann erfüllbar ist, wenn ihre Skolemform erfüllbar ist. Des Weiteren ist die Skolemform ein hilfreicher Zwischenschritt, wenn man eine Formel in Klausel-Normalform umformen will. Sie wird auch als Zwischenergebnis benötigt, wenn man ein Herbrand-Universum erzeugen will. |
| lexicalization | deu: Skolemform |
| French |
| has gloss | fra: En logique mathématique, la skolémisation dune formule du calcul des prédicats est une transformation de cette formule, qui, dans le cas dune forme prénexe, consiste à éliminer toutes les occurrences de quantificateur existentiel en utilisant de nouveaux symboles de fonction (un par quantification existentielle), ce de façon à conserver la satisfaisabilité de la formule. |
| lexicalization | fra: Skolemisation |
| lexicalization | fra: skolémisation |
| Hungarian |
| has gloss | hun: A Skolem-normálforma (SNF) a matematikai logika elsőrendű logika nevű ágában egy elsőrendű nyelv speciális szimbólumokkal, a Skolem-szimbólumokkal bővített változatának olyan formulája, melynek egyetlen valódi részformulája sem kvantált (mert „a kvantorok mind a formula legelején vannak”, azaz prenex állapotban), továbbá ha előfordul a formulában kvantor, akkor az csak univerzális kvantor lehet. |
| lexicalization | hun: Skolem-normálforma |
| Italian |
| has gloss | ita: In logica matematica, si dice skolemizzazione lapplicazione dellalgoritmo di Skolem che trasforma un enunciato in forma normale in un enunciato universale. Lenunciato in questione,dopo lapplicazione dellalgoritmo di Skolem, perde lequivalenza semantica con l'enunciato di partenza. È interessante però constatare che rimane invariata la soddisfacibilità. |
| lexicalization | ita: Skolemizzazione |
| Japanese |
| has gloss | jpn: スコーレム標準形（英: Skolem normal form）とは、冠頭標準形に全称量化子しか含まれない一階述語論理の論理式の形式である。名称の由来はトアルフ・スコーレム。全ての一階述語論理の論理式はスコーレム標準形に変換でき、そのスコーレム化（Skolemization）に際して充足可能性は変化しない。スコーレム化によって得られる式は元の式と等価とは限らないが、元の式が充足されるときのみ充足される。 |
| lexicalization | jpn: スコーレム標準形 |
| Polish |
| has gloss | pol: Skolemizacja to metoda pozwalająca na opuszczanie kwantyfikatorów egzystencjalnych lub też wszystkich kwantyfikatorów w formułach rachunku predykatów pierwszego rzędu zapisanych w formie preneksowej. Jej twórcą był norweski matematyk Thoralf Skolem. |
| lexicalization | pol: Skolemizacja |
| Portuguese |
| has gloss | por: Uma fórmula da lógica de primeira ordem está na forma normal de Skolem (nome devido à Thoralf Skolem), se sua forma normal prenex contiver somente quantificadores universais. Cada fórmula de primeira ordem pode ser convertida na forma normal de Skolem através do processo de skolemização. A fórmula resultante deste processo não é necessariamente equivalente à original, mas é satisfatível se e somente se a original também o for. |
| lexicalization | por: skolemização |
| Castilian |
| has gloss | spa: Una fórmula de la lógica de primer orden se considera expresada en forma normal de Skolem si su forma normal prenexa solamente contiene cuantificadores universales. Una fórmula puede ser Skolemizada, lo que implica que sus cuantificadores existenciales son suprimidos, produciendo una nueva fórmula equisatisfactible con respecto a la original. |
| lexicalization | spa: Forma normal de skolem |
| Ukrainian |
| has gloss | ukr: У логіці першого порядку деяка логічна формула є записаною в нормальній формі Сколема , якщо вона має вигляд: :\forall x_1 \forall x_2 \ldots \forall x_n A(x_1,x_2,\ldots,x_n) |
| lexicalization | ukr: Нормальна форма Сколема |
| Chinese |
| has gloss | zho: 一阶逻辑的公式是Skolem 范式的，如果它的前束范式只有全称量词。一个公式可以被Skolem 化，就是说消除它的存在量词并生成最初的公式的等价可满足的公式。Skolem 化是如下(二阶的)等价的应用 |
| lexicalization | zho: 斯科伦范式 |