In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled Skolemnization). The resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable.
| Attributes | Values |
|---|
| rdfs:label
| - Forma normal de Skolem (ca)
- Skolemform (de)
- Forma normal de Skolem (es)
- Forme normale de Skolem (fr)
- Forma normale di Skolem (it)
- 스콜렘 표준형 (ko)
- スコーレム標準形 (ja)
- Skolem normal form (en)
- Forma normal de Skolem (pt)
- Нормальна форма Сколема (uk)
- 斯科伦范式 (zh)
|
| rdfs:comment
| - 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. La skolemización es una aplicación de la equivalencia (aplicación perteneciente a la lógica de segundo orden). (es)
- スコーレム標準形（スコーレムひょうじゅんけい、英: Skolem normal form）とは、数理論理学において一階述語論理における存在記号がすべて全称記号の前にある冠頭標準形の論理式を言う。 トアルフ・スコーレムによるスコーレムの定理により、第一階述語論理における任意の論理式に対して、演繹的に等価（deductive equivalence）なスコーレム標準形の論理式が存在する。 (ja)
- 수리논리학에서 스콜렘 표준형(Skolem normal form)은 보편 양화사만으로 이루어진 프리넥스 표준형 1차 논리식을 가리킨다. 모든 1차 논리식들은 스콜렘화(Skolemization)라는 과정을 통해 그 충족가능성(satisfiability)을 변화시키지 않은 채 스콜렘 표준형으로 변환될 수 있다. 여기서 결과의 논리식이 반드시 원래의 식과 동치인 것은 아니나, 서로 모델론적으로는 일치한다: 곧, 어느 한 쪽이 충족가능하다는 것과 다른 쪽이 충족가능하다는 것이 동치이다. 스콜렘화는 논리적 진술로부터 존재 양화사를 모두 제거해나가는 방식으로 이루어진다. (ko)
- У логіці першого порядку деяка логічна формула є записаною в нормальній формі Сколема , якщо вона має вигляд: де формула записана в кон'юнктивній нормальній формі, тобто є кон'юнкцією диз'юнкцій атомарних формул чи їх заперечень. Будь-яка формула логіки першого порядку може бути зведена до формули у нормальній формі Сколема за допомогою процесу, що отримав назву сколемізація. Одержана внаслідок сколемізації формула не є логічно еквівалентна вихідній формулі, проте вона є виконуваною в тому і тільки тому випадку коли такою є вихідна формула (тобто для деякої формули існує модель в тому і тільки тому випадку, коли вона існує для формули одержаної внаслідок процесу сколемізації) . (uk)
- 如果一阶逻辑式的前束范式只有全称量词，则称其为是符合Skolem 范式的。一个公式可以被Skolem 化，就是说消除它的存在量词并生成最初的公式的的公式。Skolem 化是如下二阶逻辑的等价应用： Skolem 化的本质是对如下形式的公式的观察 它在某个模型中是可满足的，在这个模型必定对于所有的 有某些点 使得 为真，并且必定存在某个函数(选择函数) 使得公式 为真。函数 f 叫做 Skolem 函数。 举例说明: 其中a为常数 (zh)
- En lògica matemàtica, la reducció a la forma normal de Skolem (FNS) és un mètode per eliminar els quantificadors existencials dels enunciats de lògica, i sovint aquest és un primer pas en la . Una fórmula de lògica de primer ordre es diu que està en forma normal de Skolem (anomenada així en honor de Thoralf Skolem) si està en conjuntiva amb només quantificadors universals de primer ordre. Tota fórmula ben formada es pot convertir en forma normal de Skolem sense alterar-ne la , mitjançant un procés anomenat skolemització. La fórmula que en resulta no és necessàriament equivalent a l'original, però hi és : és satisfactible si i només si la fórmula original és satisfactible. (ca)
- Die Skolemform gehört zu den mathematischen Darstellungen der Prädikatenlogik, um Argumente zu formalisieren und auf ihre Gültigkeit zu überprüfen. Die Skolemform ist eine logische Formel mit Variablen, die keinen Quantifikator, kurz Quantor zur Existenz hat, also ohne „es existiert“. Diese Form wurde nach dem norwegischen Mathematiker Albert Thoralf Skolem (1887–1963) benannt. (de)
- In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled Skolemnization). The resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable. (en)
|
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| id
| |
| title
| - Skolem function (en)
- SkolemizedForm (en)
|
| urlname
| |
| has abstract
| - En lògica matemàtica, la reducció a la forma normal de Skolem (FNS) és un mètode per eliminar els quantificadors existencials dels enunciats de lògica, i sovint aquest és un primer pas en la . Una fórmula de lògica de primer ordre es diu que està en forma normal de Skolem (anomenada així en honor de Thoralf Skolem) si està en conjuntiva amb només quantificadors universals de primer ordre. Tota fórmula ben formada es pot convertir en forma normal de Skolem sense alterar-ne la , mitjançant un procés anomenat skolemització. La fórmula que en resulta no és necessàriament equivalent a l'original, però hi és : és satisfactible si i només si la fórmula original és satisfactible. La forma més senzilla de skolemització es dona en el cas de variables amb quantificació existencial que no estan dins l'àmbit d'un quantificador universal. Aquestes variables es poden substituir per noves constants. Per exemple, es pot canviar a , on és una nova constant (ja que no apareix enlloc més de la fórmula). Més en general, la skolemització es realitza mitjançant la substitució de tota variable quantificada existencialment per un terme , on la funció és nova. Les variables d'aquest terme són de la següent forma: si la fórmula està en , són les variables quantificades universalment per quantificadors situats abans del quantificador de . En general, són les variables que estan quantificades universalment, i tals que apareix en l'àmbit d'aquests altres quantificadors universals. La funció introduïda en aquest procés és anomenada funció de Skolem (o constant de Skolem, si té aritat zero), i el terme s'anomena terme de Skolem. Com a exemple, la fórmula no està en forma normal de Skolem, perquè conté el quantificador existencial . La skolemització substitueix per , on és una nova funció, i elimina la quantificació sobre . La fórmula resultant és . El terme de Skolem conté però no , perquè el quantificador que s'havia d'eliminar estava dins l'àmbit de però no del de ; com que aquesta fórmula està en forma normal prenexa, això és equivalent a dir que, en la llista de quantificadors, precedeix , mentre que no ho fa. La fórmula obtinguda mitjançant aquest procés és satisfactible si i només si ho és la fórmula original. (ca)
- Die Skolemform gehört zu den mathematischen Darstellungen der Prädikatenlogik, um Argumente zu formalisieren und auf ihre Gültigkeit zu überprüfen. Die Skolemform ist eine logische Formel mit Variablen, die keinen Quantifikator, kurz Quantor zur Existenz hat, also ohne „es existiert“. Diese Form wurde nach dem norwegischen Mathematiker Albert Thoralf Skolem (1887–1963) benannt. Logische Formeln sind erfüllbar, wenn mindestens eine Belegung der Variablen zu einer wahren Aussage führt. Algorithmen zur Prüfung der Erfüllbarkeit nutzen oft die Skolemform, da jede Formel genau dann erfüllbar ist, wenn ihre Skolemform erfüllbar ist. Die Skolemform ist ferner ein praktischer Zwischenschritt, wenn eine logische Formel in die Klausel-Normalform umgeformt werden soll oder bei der Erzeugung eines Herbrand-Universums. Die Skolemform hat keine Existenzquantoren , alle Ausdrücke sind aufgelöst. bedeutet „es existiert mindests ein “ – mit einer bestimmten Eigenschaft. Variablen , die an Existenzquantoren gebunden sind, werden durch neue Funktions- oder Konstantensymbole ersetzt. Die Argumente der neuen Funktionssymbole haben Allquantoren – sprich: "es gilt für alle ". (de)
- 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. La skolemización es una aplicación de la equivalencia (aplicación perteneciente a la lógica de segundo orden). (es)
- In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled Skolemnization). The resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable. Reduction to Skolem normal form is a method for removing existential quantifiers from formal logic statements, often performed as the first step in an automated theorem prover. (en)
- スコーレム標準形（スコーレムひょうじゅんけい、英: Skolem normal form）とは、数理論理学において一階述語論理における存在記号がすべて全称記号の前にある冠頭標準形の論理式を言う。 トアルフ・スコーレムによるスコーレムの定理により、第一階述語論理における任意の論理式に対して、演繹的に等価（deductive equivalence）なスコーレム標準形の論理式が存在する。 (ja)
- 수리논리학에서 스콜렘 표준형(Skolem normal form)은 보편 양화사만으로 이루어진 프리넥스 표준형 1차 논리식을 가리킨다. 모든 1차 논리식들은 스콜렘화(Skolemization)라는 과정을 통해 그 충족가능성(satisfiability)을 변화시키지 않은 채 스콜렘 표준형으로 변환될 수 있다. 여기서 결과의 논리식이 반드시 원래의 식과 동치인 것은 아니나, 서로 모델론적으로는 일치한다: 곧, 어느 한 쪽이 충족가능하다는 것과 다른 쪽이 충족가능하다는 것이 동치이다. 스콜렘화는 논리적 진술로부터 존재 양화사를 모두 제거해나가는 방식으로 이루어진다. (ko)
- У логіці першого порядку деяка логічна формула є записаною в нормальній формі Сколема , якщо вона має вигляд: де формула записана в кон'юнктивній нормальній формі, тобто є кон'юнкцією диз'юнкцій атомарних формул чи їх заперечень. Будь-яка формула логіки першого порядку може бути зведена до формули у нормальній формі Сколема за допомогою процесу, що отримав назву сколемізація. Одержана внаслідок сколемізації формула не є логічно еквівалентна вихідній формулі, проте вона є виконуваною в тому і тільки тому випадку коли такою є вихідна формула (тобто для деякої формули існує модель в тому і тільки тому випадку, коли вона існує для формули одержаної внаслідок процесу сколемізації) . (uk)
- 如果一阶逻辑式的前束范式只有全称量词，则称其为是符合Skolem 范式的。一个公式可以被Skolem 化，就是说消除它的存在量词并生成最初的公式的的公式。Skolem 化是如下二阶逻辑的等价应用： Skolem 化的本质是对如下形式的公式的观察 它在某个模型中是可满足的，在这个模型必定对于所有的 有某些点 使得 为真，并且必定存在某个函数(选择函数) 使得公式 为真。函数 f 叫做 Skolem 函数。 举例说明: 其中a为常数 (zh)
|
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)