| Property |
Value |
| 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. (es)
- 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. (es)
|
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
| |
| dbo:wikiPageRevisionID
| |
| prop-es:authorlink
|
- Martin Davis (es)
- Martin Davis (es)
|
| prop-es:coauthors
| |
| prop-es:date
|
- 1960 (xsd:integer)
- 1962 (xsd:integer)
|
| prop-es:doi
|
- 101016 (xsd:integer)
- 101145 (xsd:integer)
|
| prop-es:first
|
- Ming (es)
- Martin (es)
- Ming (es)
- Martin (es)
|
| prop-es:issue
|
- 1 (xsd:integer)
- 3 (xsd:integer)
- 7 (xsd:integer)
|
| prop-es:journal
| |
| prop-es:last
|
- Ouyang (es)
- Davis (es)
- Ouyang (es)
- Davis (es)
|
| prop-es:pages
|
- 201 (xsd:integer)
- 281 (xsd:integer)
- 394 (xsd:integer)
|
| prop-es:title
|
- A Computing Procedure for Quantification Theory (es)
- A Machine Program for Theorem Proving (es)
- How Good Are Branching Rules in DPLL? (es)
- A Computing Procedure for Quantification Theory (es)
- A Machine Program for Theorem Proving (es)
- How Good Are Branching Rules in DPLL? (es)
|
| prop-es:url
| |
| prop-es:volume
|
- 5 (xsd:integer)
- 7 (xsd:integer)
- 89 (xsd:integer)
|
| prop-es:year
| |
| dct:subject
| |
| 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. (es)
- 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. (es)
|
| rdfs:label
|
- Algoritmo DPLL (es)
- Algoritmo DPLL (es)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is owl:sameAs
of | |
| is foaf:primaryTopic
of | |
