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

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

PrefixNamespace IRI
category-eshttp://es.dbpedia.org/resource/Categoría:
dcthttp://purl.org/dc/terms/
wikipedia-eshttp://es.wikipedia.org/wiki/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
dbpedia-eshttp://es.dbpedia.org/resource/
prop-eshttp://es.dbpedia.org/property/
n10http://redalyc.uaemex.mx/redalyc/pdf/925/92572004.
rdfshttp://www.w3.org/2000/01/rdf-schema#
n7http://portal.acm.org/citation.cfm%3Fdoid=368273.
n14http://rdf.freebase.com/ns/m.
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
dbrhttp://dbpedia.org/resource/
n12http://es.wikipedia.org/wiki/Algoritmo_DPLL?oldid=120190748&ns=
n5http://portal.acm.org/citation.cfm%3Fcoll=GUIDE&dl=GUIDE&id=
Subject Item
dbpedia-es:Algoritmo_DPLL
rdfs:label
Algoritmo DPLL
rdfs:comment
El algoritmo DPLL/Davis-Putnam-Logemann-Loveland es un algoritmo completo basado en la vuelta atrás que sirve para decidir la satisfactibilidad de las fórmulas de lógica proposicional en una forma normal conjuntiva, es decir, para resolver el problema . El DPLL es un procedimiento muy eficiente y tras más de 40 años aún conforma la base de los solucionadores más eficaces de SAT, así como de muchos demostradores de teoremas para fragmentos de lógica de primer orden.
owl:sameAs
n14:080fyp
dct:subject
category-es:Algoritmos_SAT
foaf:isPrimaryTopicOf
wikipedia-es:Algoritmo_DPLL
prop-es:authorlink
Martin Davis
prop-es:coauthors
dbpedia-es:Hillary_Putnam Logemann, George, and Loveland, Donald
prop-es:date
1960 1962
prop-es:doi
101145 101016
prop-es:first
Martin Ming
prop-es:issue
1 3 7
prop-es:journal
dbpedia-es:Communications_of_the_ACM Discrete Applied Mathematics dbpedia-es:Journal_of_the_ACM
prop-es:last
Ouyang Davis
prop-es:pages
201 281 394
prop-es:title
How Good Are Branching Rules in DPLL? A Machine Program for Theorem Proving A Computing Procedure for Quantification Theory
prop-es:url
n5:321034 n7:368557
prop-es:volume
89 5 7
prop-es:year
1998
dbo:wikiPageID
771951
dbo:wikiPageRevisionID
120190748
dbo:wikiPageExternalLink
n5:321034 n7:368557 n10:pdf
dbo:wikiPageLength
5714
prov:wasDerivedFrom
n12:0
dbo:abstract
El algoritmo DPLL/Davis-Putnam-Logemann-Loveland es un algoritmo completo basado en la vuelta atrás que sirve para decidir la satisfactibilidad de las fórmulas de lógica proposicional en una forma normal conjuntiva, es decir, para resolver el problema . Fue presentado en 1962 por Martin Davis, Hilary Putnam, y y es una refinación del previo algoritmo de Davis-Putnam, el cual es un procedimiento de resolución desarrollado por Davis y Putnam en 1960. El algoritmo Davis-Putnam-Logemann-Loveland es nombrado a menudo como el "método Davis-Putnam" o el "algoritmo DP", especialmente en publicaciones antiguas. Otros nombres comunes que mantienen la distinción son DLL y DPLL. El DPLL es un procedimiento muy eficiente y tras más de 40 años aún conforma la base de los solucionadores más eficaces de SAT, así como de muchos demostradores de teoremas para fragmentos de lógica de primer orden.
Subject Item
wikipedia-es:Algoritmo_DPLL
foaf:primaryTopic
dbpedia-es:Algoritmo_DPLL
Subject Item
dbr:DPLL_algorithm
owl:sameAs
dbpedia-es:Algoritmo_DPLL