| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:label
| - Algorithme de Davis-Putnam (fr)
- Davis–Putnam algorithm (en)
- Алгоритм Дэвиса — Патнема (ru)
- デービス・パトナムのアルゴリズム (ja)
|
| 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. (fr)
|
| sameAs
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| dbo:wikiPageWikiLink
| |
| Link from a Wikipage to an external page
| |
| page length (characters) of wiki page
| |
| dct:subject
| |
| prop-fr:wikiPageUsesTemplate
| |
| prov:wasDerivedFrom
| |
| prop-fr:année
| |
| prop-fr:auteur
| |
| prop-fr:doi
| |
| prop-fr:journal
| |
| prop-fr:langue
| |
| prop-fr:numéro
| |
| prop-fr:pages
| |
| prop-fr:titre
| - A Computing Procedure for Quantification Theory (fr)
|
| prop-fr:url
| |
| prop-fr:volume
| |
| foaf:isPrimaryTopicOf
| |
| named after
| |
| has 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. (fr)
|
| is dbo:wikiPageWikiLink
of | |
| is Wikipage redirect
of | |
| is Wikipage disambiguates
of | |
| is prop-fr:renomméPour
of | |
| is oa:hasTarget
of | |
| is foaf:primaryTopic
of | |
| is known for
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)