This HTML5 document contains 64 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dbpedia-dehttp://de.dbpedia.org/resource/
dcthttp://purl.org/dc/terms/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
dbpedia-cahttp://ca.dbpedia.org/resource/
n20http://portal.acm.org/
dbpedia-eshttp://es.dbpedia.org/resource/
n18http://g.co/kg/m/
dbpedia-ruhttp://ru.dbpedia.org/resource/
rdfshttp://www.w3.org/2000/01/rdf-schema#
category-frhttp://fr.dbpedia.org/resource/Catégorie:
dbpedia-plhttp://pl.dbpedia.org/resource/
dbpedia-pthttp://pt.dbpedia.org/resource/
n14http://fr.dbpedia.org/resource/Modèle:
wikipedia-frhttp://fr.wikipedia.org/wiki/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n25http://ma-graph.org/entity/
dbpedia-ithttp://it.dbpedia.org/resource/
dbpedia-frhttp://fr.dbpedia.org/resource/
prop-frhttp://fr.dbpedia.org/property/
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/
dbpedia-jahttp://ja.dbpedia.org/resource/

Statements

Subject Item
dbpedia-fr:Algorithme_de_Davis-Putnam
rdf:type
owl:Thing dbo:Algorithm wikidata:Q8366
rdfs:label
Davis–Putnam algorithm Algorithme de Davis-Putnam Алгоритм Дэвиса — Патнема デービス・パトナムのアルゴリズム
rdfs:comment
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.
owl:sameAs
dbpedia-ca:Algorisme_de_Davis-Putnam dbpedia-es:Algoritmo_de_Davis-Putnam dbpedia-de:Davis-Putnam-Verfahren dbpedia-pt:Algoritmo_de_Davis-Putnam dbr:Davis–Putnam_algorithm n18:07_p4x wikidata:Q1177898 dbpedia-it:Algoritmo_di_Davis-Putnam dbpedia-ru:Алгоритм_Дэвиса_—_Патнема dbpedia-pl:Procedura_Davisa-Putnama dbpedia-ja:デービス・パトナムのアルゴリズム n25:2780912396
dbo:wikiPageID
1116536
dbo:wikiPageRevisionID
150153456
dbo:wikiPageWikiLink
dbpedia-fr:Martin_Davis dbpedia-fr:Algorithme_DPLL dbpedia-fr:Conjonction_logique dbpedia-fr:Journal_of_the_ACM dbpedia-fr:Disjonction dbpedia-fr:Terminaison_d'un_algorithme dbpedia-fr:Forme_normale_conjonctive dbpedia-fr:Formule_(mathématiques) dbpedia-fr:Problème_SAT category-fr:Algorithme dbpedia-fr:Clause_de_Horn dbpedia-fr:Littéral dbpedia-fr:Hilary_Putnam category-fr:Logique dbpedia-fr:Calcul_des_prédicats dbpedia-fr:Clause_(logique) dbpedia-fr:Calcul_des_propositions dbpedia-fr:Tautologie dbpedia-fr:Règle_de_résolution
dbo:wikiPageExternalLink
n20:citation.cfm%3Fcoll=GUIDE&dl=GUIDE&id=321034
dbo:wikiPageLength
5259
dct:subject
category-fr:Logique category-fr:Algorithme
prop-fr:wikiPageUsesTemplate
n14:Article n14:Portail n14:Ébauche
prov:wasDerivedFrom
wikipedia-fr:Algorithme_de_Davis-Putnam?oldid=150153456&ns=0
prop-fr:année
1960
prop-fr:auteur
dbpedia-fr:Martin_Davis dbpedia-fr:Hilary_Putnam
prop-fr:doi
10.1145
prop-fr:journal
dbpedia-fr:Journal_of_the_ACM
prop-fr:langue
en
prop-fr:numéro
3
prop-fr:pages
201
prop-fr:titre
A Computing Procedure for Quantification Theory
prop-fr:url
n20:citation.cfm%3Fcoll=GUIDE&dl=GUIDE&id=321034
prop-fr:volume
7
foaf:isPrimaryTopicOf
wikipedia-fr:Algorithme_de_Davis-Putnam
dbo:namedAfter
dbpedia-fr:Hilary_Putnam dbpedia-fr:Martin_Davis
dbo:abstract
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.