En lógica matemática , una interpretación de Herbrand es una interpretación en la que a todas las constantes y símbolos de función se les asignan significados muy simples. [1] Específicamente, cada constante se interpreta como sí misma, y cada símbolo de función se interpreta como la función que lo aplica. La interpretación también define los símbolos predicados como que denotan un subconjunto de la base Herbrand relevante , especificando efectivamente qué átomos fundamentales son verdaderos en la interpretación. Esto permite que los símbolos de un conjunto de cláusulas se interpreten de forma puramente sintáctica , separados de cualquier instanciación real.
La importancia de las interpretaciones de Herbrand es que, si alguna interpretación satisface un conjunto dado de cláusulas S, entonces existe una interpretación de Herbrand que las satisface. Por otra parte, el teorema de Herbrand establece que si S es unsatisfiable continuación, hay un conjunto unsatisfiable finito de instancias de tierra del universo Herbrand definido por S . Dado que este conjunto es finito, su insatisfacción se puede verificar en un tiempo finito. Sin embargo, puede haber un número infinito de estos conjuntos para comprobar.
Lleva el nombre de Jacques Herbrand .
Ver también
Notas
- ^ Ben Coppin (2004). Inteligencia artificial iluminada . Jones y Bartlett Learning. pag. 231. ISBN 978-0-7637-3230-1.