| rdfs:comment
| - Horn-Formeln sind eine wichtige Art prädikatenlogischer Formeln. Sie spielen eine zentrale Rolle in der logischen Programmierung und sind von Bedeutung für die konstruktive Logik. Benannt wurden sie nach dem US-amerikanischen Mathematiker Alfred Horn. (de)
- In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form which gives it useful properties for use in logic programming, formal specification, and model theory. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951. (en)
- ホーン節（ホーンせつ、英: Horn clause）とは、数理論理学において、節（リテラルの選言結合命題）のうち、肯定形のリテラルの数が1つ以下の物を言う。論理学者のアルフレッド・ホーンによって導入された。 (ja)
- In de logica is een Horn-clausule (Engels: Horn clause) een clausule, een disjunctie van literalen, met ten hoogste 1 positieve literaal. Ze zijn vernoemd naar de logicus , die deze in 1951 behandelde in zijn publicatie "On sentences which are true of direct unions of algebras" in . Horn-clausules zijn van belang bij logisch programmeren en intuïtionistische logica (ook constructieve logica genoemd). (nl)
- Хорновский дизъюнкт — дизъюнктивный одночлен с не более чем одним положительным литералом. Изучены (англ. Alfred Horn) в 1951 году в связи с их важной ролью в теории моделей и универсальной алгебре. Впоследствии стали основой для языка логического программирования Пролог, в котором программа являются непосредственно набором хорновских дизъюнктов, а также нашли важные приложения в конструктивной логике и теории сложности вычислений. (ru)
- 在数理逻辑中，霍恩子句（Horn Clause）是带有最多一个肯定文字的子句(文字的析取)。霍恩子句得名于逻辑学家 ，他在 1951 年首先在文章《On sentences which are true of direct unions of algebras》, Journal of Symbolic Logic, 16, 14-21 中指出这种子句的重要性。 有且只有一个肯定文字的霍恩子句叫做明确子句，没有任何肯定文字的霍恩子句叫做目标子句。霍恩子句的合取是合取范式，也叫做 霍恩公式。霍恩子句在逻辑编程中扮演基本角色并且在构造性逻辑中很重要。 下面是一个霍恩子句的例子： ， 它可以被等价地写为： 。 霍恩子句对定理证明的实用性是一阶归结提供的，两个霍恩子句的归结是一个霍恩子句。在自动定理证明中，这能导致子句的在计算机上表示得更加高效。实际上，Prolog 就是完全在霍恩子句上构造的编程语言。 霍恩子句在计算复杂性中也是关键的，在这里找到一组变量指派使霍恩子句的合取的为真的问题是一个P-完全问题，有时叫做 HORNSAT。这是布尔可满足性问题的 P 的变体，它是一个中心的NP-完全问题。 (zh)
- В математичній логіці та логічному програмуванні диз'ю́нкт Го́рна (англ. Horn clause) — це логічна формула певного правилоподібного вигляду, який надає їй корисних властивостей для застосування в логічному програмуванні, формальних специфікаціях та теорії моделей. Диз'юнкти Горна названо на честь логіка , який першим 1951 року зазначив їхню важливість. (uk)
- En lògica proposicional, una fórmula lògica és una clàusula de Horn si és una clàusula (disjunció de literals) amb, com a màxim, un literal positiu. Es diuen així pel lògic Alfred Horn, el primer a assenyalar la importància d'aquestes clàusules en 1951. Això és un exemple d'una clàusula de Horn: Una fórmula com aquesta també pot reescriure's de forma equivalent com una implicació: Una fórmula de Horn és una cadena textual (string) de quantificadors existencials o universals seguits per una conjunció de clàusules de Horn. (ca)
- Ve výrokové logice se jako Hornova klauzule označuje speciální druh klauzule (disjunkce literálů), která obsahuje nejvýše jeden pozitivní literál (ostatní jsou negované): . Hornovu klauzuli tak lze obecně zapsat jako implikaci ve formě: . Jako Hornova formule se pak označuje formule v konjunktivní normální formě, která se skládá z Hornových klauzulí. Jako duální Hornova klauzule se pak označuje klauzule, která obsahuje nejvýše jeden negativní literál (a ostatní pozitivní). (cs)
- En lógica proposicional, una fórmula lógica es una cláusula de Horn si es una cláusula (disyunción de literales) con, como máximo, un literal positivo. Se llaman así por el lógico Alfred Horn, el primero en señalar la importancia de estas cláusulas en 1951. Esto es un ejemplo de una cláusula de Horn: Una fórmula como esta también puede reescribirse de forma equivalente como una implicación: Una fórmula de Horn es una cadena textual (string) de cuantificadores existenciales o universales seguidos por una conjunción de cláusulas de Horn. (es)
- En logique, en particulier en calcul propositionnel, une clause de Horn est une clause comportant au plus un littéral positif. Il existe donc trois types de clauses de Horn :
* celles qui comportent un littéral positif et au moins un littéral négatif, appelées clauses de Horn strictes ;
* celles qui comportent un littéral positif et aucun littéral négatif, appelées clauses de Horn positives ;
* celles qui ne comportent que des littéraux négatifs, appelées clauses de Horn négatives. (fr)
- In logica, e in particolare nel calcolo proposizionale, una clausola di Horn è una disgiunzione di letterali in cui al massimo uno dei letterali è positivo. Prendono il nome da che per primo ne evidenziò l'importanza (1951). Un esempio di clausola di Horn è il seguente: Il numero dei letterali può essere arbitrario (anche zero); la condizione che al massimo uno sia positivo permette di scrivere la clausola sotto forma di implicazione. Partendo dall'esempio, applichiamo prima De Morgan: Dopodiché utilizziamo l'equivalenza logica: Ricaviamo quindi: (it)
- Em lógica, uma cláusula de Horn é uma cláusula (disjunção de literais) com no máximo um literal positivo. O nome "Cláusula de Horn" é uma homenagem ao lógico Alfred Horn, que foi quem primeiro chamou a atenção para o valor destas cláusulas, em 1951, no artigo "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21. Uma cláusula de Horn pode ser de quatro tipos diferentes: Em Prolog isto se escreve como: u :- p, q, … , t Usando a lógica clássica proposicional, tal fórmula pode ser reescrita ainda, de forma equivalente, da seguinte forma: (pt)
- Klauzula Horna (ang. Horn clause) – klauzula, w której co najwyżej jeden element jest niezanegowany. Przykładami takich klauzul są {p,¬r,¬q} i {¬r,¬q}. Klauzule Horna zapisuje się zwykle w postaci implikacyjnej:
* p ← r ∧ q
* ← r ∧ q albo w prologowskiej:
* p :- r, q
* :- r, q Klauzule Horna są używane w programowaniu logicznym (na przykład w Prologu). Wykorzystywane są również do reprezentowania wiedzy w systemach eksperckich, ponieważ spełniają ważną właściwość: klauzula jest równoważna Można wyróżnić trzy rodzaje klauzul Horna: (pl)
|
![[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)