An Entity of Type: Procedure101023820, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm.

Property Value
dbo:abstract
  • L'algorisme de Davis-Putnam va ser desenvolupat per Martin Davis i Hilary Putnam per comprovar la satisfacibilitat de les fórmules de la lògica proposicional en forma normal conjuntiva, és a dir, en conjunts de clàusules. Això és una forma de resolució en la qual les variables són triades iterativament i eliminades mitjançant la resolució de cada clàusula en la qual la variable apareix afirmada amb una clàusula en la qual la variable és negada. L'algorisme és així: * per a cada variable en la fórmula * per a cada clàusula que continga la variable i cada clàusula que continga la negació de la variable * resoldre i i afegir la resolució a la fórmula * eliminar totes les clàusules originals que continguen la variable o la seva negació El nom algorisme Davis-Putnam o algorisme DP de vegades és emprat incorrectament per referir-se a l', el qual està relacionat però és diferent. (ca)
  • Das Davis-Putnam-Verfahren (nach Martin Davis und Hilary Putnam) entscheidet über die Unerfüllbarkeit einer aussagenlogischen Formel in konjunktiver Normalform. Das Verfahren sollte nicht mit der Weiterentwicklung, dem (Davis-Putnam-Logemann-Loveland)-Algorithmus, verwechselt werden. (de)
  • The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm. (en)
  • El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en forma normal conjuntiva, es decir, en conjuntos de cláusulas. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada. El algoritmo es como sigue: * para cada variable en la fórmula * para cada cláusula que contenga la variable y cada cláusula que contenga la negación de la variable * resolver y y añadir la resolución a la fórmula * eliminar todas las cláusulas originales que contengan la variable o su negación El nombre algoritmo Davis-Putnam o algoritmo DP a veces es empleado incorrectamente para referirse al algoritmo DPLL, el cual está relacionado pero es diferente. (es)
  • En calcul propositionnel, l'algorithme de Davis-Putnam est une méthode de détermination de la satisfiabilité d'une formule en forme normale conjonctive, c'est-à-dire une conjonction de clauses (disjonctions de littéraux). Il a été développé par Martin Davis et Hilary Putnam. Cet algorithme a d'abord été conçu pour l'obtention automatique de preuves en calcul des prédicats, mais sa principale innovation concerne la réfutation automatique d'un ensemble de clauses. Comme son dérivé plus connu, l'algorithme DPLL, l'algorithme de Davis-Putnam utilise la propagation unitaire et l'élimination des littéraux purs. Mais l'appel récursif utilisé dans l'algorithme DPLL est remplacé par l'utilisation exhaustive de la règle de résolution sur une variable. L'algorithme de Davis-Putnam permet de prouver qu'un ensemble de clauses est satisfiable (ou non), mais contrairement à l'algorithme DPLL, il ne donne pas directement une affectation satisfaisant cet ensemble de clauses. (fr)
  • デービス・パトナムのアルゴリズム(英: Davis–Putnam algorithm)は、与えられた論理式の充足可能性を調べるアルゴリズムで、連言標準形で表現された命題論理式を対象とする。アメリカ国家安全保障局の支援を受け、一階述語論理での定理自動証明のための方法として(Martin Davis)とヒラリー・パトナム(Hilary Putnam)により1958年に考案され、一般には1960年に発表された。その後の改良版であるDPLLアルゴリズム(Davis-Putnam-Logemann-Loveland algorithm)のベースとなるアルゴリズムである。 なお、古い文献ではDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。1960年に提案されたデービス・パトナムのアルゴリズムが導出を使用するのに対し、1962年に提案されたDPLLアルゴリズムはバックトラックを使用する。 (ja)
  • Procedura Davisa-Putnama – bardzo efektywny system dowodzenia twierdzeń dla rachunku zdań. Istnieją też jego modyfikacje dla rachunku predykatów pierwszego rzędu, jednak są one zwykle mniej wydajne od rezolucji. Idea jest następująca: negację formuły, którą zamierzamy udowodnić zamieniamy na alternatywę koniunkcji alternatyw literałów, czyli alternatywę CNFów. Taki CNF nazywa się tu zbiorem klauzul, natomiast alternatywa CNFów blokiem. Następnie usuwamy wszystkie powtórzenia literałów i fałsze, oraz wszystkie klauzule zawierające jednocześnie literał i jego negację lub też prawdę. Reguły systemu: * subsumpcja – jeśli w pewnym zbiorze klauzul klauzula C subsumuje klauzulę D, czyli wszystkie literały C występują też w D, to usuwamy D * jeśli w pewnym zbiorze klauzul jakiś literał występuje tylko pozytywnie lub tylko negatywnie, usuwamy z niego wszystkie klauzule które go zawierają * jeśli w pewnym zbiorze klauzul jakaś klauzula to pojedynczy literał, usuwamy wszystkie klauzule zawierające ten literał, oraz zaprzeczenie tego literału z wszystkich klauzul zbioru, które go zawierały * splitting – jeśli w pewnym zbiorze klauzul pewien literał występuje zarówno pozytywnie jak i negatywnie zastępujemy cały zbiór dwoma zbiorami: * jednym, w którym usunięte zostały wszystkie klauzule zawierające ten literał, oraz wszystkie wystąpienia jego negacji * drugim, w którym usunięte zostały wszystkie wystąpienia tego literału, oraz wszystkie klauzule zawierające jego negację * usuwamy każdy zbiór klauzul zawierają klauzulę pustą – klauzula ta usuwa wszystkie inne przez subsumpcje i ma wartość fałsz, a co za tym idzie zbiór klauzul ma wartość fałsz, która jest nieistotna dla bloku będącego alternatywą Jeśli w bloku nie ma już zbiorów klauzul twierdzenie zostało udowodnione (taki blok, jako alternatywa, jest fałszywy – skoro negacja formuły jest fałszywa, to twierdzenie to jest prawdziwe). Jeśli został jakiś pusty zbiór klauzul, twierdzenie to jest fałszywe (jego zaprzeczenie jest spełnialne). (pl)
  • O Algoritmo de Davis-Putnam, criado por Martin Davis e Hilary Putnam, foi um dos pioneiros na área de checagem da satisfatibilidade de uma fórmula quando essa encontra-se na Forma Normal Conjuntiva (FNC). É uma forma de resolução em que cada variável é escolhida pelo fato de se poder resolver todas as cláusulas em que a mesma está contida na sua forma positiva com qualquer cláusula em que ela encontre-se em sua forma negada. (pt)
dbo:thumbnail
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 2732435 (xsd:integer)
dbo:wikiPageLength
  • 7042 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1071405701 (xsd:integer)
dbo:wikiPageWikiLink
dbp:date
  • June 2021 (en)
dbp:reason
  • In the algorithm below, adding to and removing from a formula should be defined. I guess the formula has to be in clausal normal form , and adding and removing is achieved by set operations? Moreover, the 'consistent set of literals' test, and the concepts 'polarity', 'pure literal' and 'unit propagation' should be briefly explained. (en)
dbp:wikiPageUsesTemplate
dct:subject
rdf:type
rdfs:comment
  • Das Davis-Putnam-Verfahren (nach Martin Davis und Hilary Putnam) entscheidet über die Unerfüllbarkeit einer aussagenlogischen Formel in konjunktiver Normalform. Das Verfahren sollte nicht mit der Weiterentwicklung, dem (Davis-Putnam-Logemann-Loveland)-Algorithmus, verwechselt werden. (de)
  • The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm. (en)
  • デービス・パトナムのアルゴリズム(英: Davis–Putnam algorithm)は、与えられた論理式の充足可能性を調べるアルゴリズムで、連言標準形で表現された命題論理式を対象とする。アメリカ国家安全保障局の支援を受け、一階述語論理での定理自動証明のための方法として(Martin Davis)とヒラリー・パトナム(Hilary Putnam)により1958年に考案され、一般には1960年に発表された。その後の改良版であるDPLLアルゴリズム(Davis-Putnam-Logemann-Loveland algorithm)のベースとなるアルゴリズムである。 なお、古い文献ではDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。1960年に提案されたデービス・パトナムのアルゴリズムが導出を使用するのに対し、1962年に提案されたDPLLアルゴリズムはバックトラックを使用する。 (ja)
  • O Algoritmo de Davis-Putnam, criado por Martin Davis e Hilary Putnam, foi um dos pioneiros na área de checagem da satisfatibilidade de uma fórmula quando essa encontra-se na Forma Normal Conjuntiva (FNC). É uma forma de resolução em que cada variável é escolhida pelo fato de se poder resolver todas as cláusulas em que a mesma está contida na sua forma positiva com qualquer cláusula em que ela encontre-se em sua forma negada. (pt)
  • L'algorisme de Davis-Putnam va ser desenvolupat per Martin Davis i Hilary Putnam per comprovar la satisfacibilitat de les fórmules de la lògica proposicional en forma normal conjuntiva, és a dir, en conjunts de clàusules. Això és una forma de resolució en la qual les variables són triades iterativament i eliminades mitjançant la resolució de cada clàusula en la qual la variable apareix afirmada amb una clàusula en la qual la variable és negada. L'algorisme és així: (ca)
  • El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en forma normal conjuntiva, es decir, en conjuntos de cláusulas. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada. El algoritmo es como sigue: (es)
  • En calcul propositionnel, l'algorithme de Davis-Putnam est une méthode de détermination de la satisfiabilité d'une formule en forme normale conjonctive, c'est-à-dire une conjonction de clauses (disjonctions de littéraux). Il a été développé par Martin Davis et Hilary Putnam. Cet algorithme a d'abord été conçu pour l'obtention automatique de preuves en calcul des prédicats, mais sa principale innovation concerne la réfutation automatique d'un ensemble de clauses. (fr)
  • Procedura Davisa-Putnama – bardzo efektywny system dowodzenia twierdzeń dla rachunku zdań. Istnieją też jego modyfikacje dla rachunku predykatów pierwszego rzędu, jednak są one zwykle mniej wydajne od rezolucji. Idea jest następująca: negację formuły, którą zamierzamy udowodnić zamieniamy na alternatywę koniunkcji alternatyw literałów, czyli alternatywę CNFów. Taki CNF nazywa się tu zbiorem klauzul, natomiast alternatywa CNFów blokiem. Następnie usuwamy wszystkie powtórzenia literałów i fałsze, oraz wszystkie klauzule zawierające jednocześnie literał i jego negację lub też prawdę. (pl)
rdfs:label
  • Algorisme de Davis-Putnam (ca)
  • Davis-Putnam-Verfahren (de)
  • Davis–Putnam algorithm (en)
  • Algoritmo de Davis-Putnam (es)
  • Algorithme de Davis-Putnam (fr)
  • デービス・パトナムのアルゴリズム (ja)
  • Algoritmo di Davis-Putnam (it)
  • Procedura Davisa-Putnama (pl)
  • Алгоритм Дэвиса — Патнема (ru)
  • Algoritmo de Davis-Putnam (pt)
owl:sameAs
prov:wasDerivedFrom
foaf:depiction
foaf:isPrimaryTopicOf
is dbo:knownFor of
is dbo:notableIdea of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is dbp:knownFor of
is dbp:notableIdeas of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License