Introducción a la verificación lógica de primer orden

9

Estoy tratando de enseñarme diferentes enfoques para la verificación de software. He leido algunos articulos. Hasta donde aprendí, la lógica proposicional con temporal generalmente usa la verificación de modelos con solucionadores SAT (en sistemas reactivos en curso), pero ¿qué pasa con la lógica de primer orden con temporal? ¿Utiliza demostradores de teoremas? ¿O también puede usar SAT?

Cualquier sugerencia de libros o artículos para principiantes en este asunto es muy apreciada.

FELIPE N.
fuente
2
Antes que nada bienvenido a CS: SE. Si bien no soy un experto en esto, parece que te estás ocupando de varios temas a la vez dejando muchos agujeros. No te preocupes Lo hago todo el tiempo. Echar un vistazo a la verificación del software a continuación, la verificación formal entonces la comprobación de modelo y formal Software Verificación: Comprobación del modelo y de demostración de teoremas
individuo Coder

Respuestas:

9

La lógica de primer orden es indecidible, por lo que la resolución SAT realmente no ayuda. Dicho esto, existen técnicas para la verificación del modelo acotado de fórmulas de primer orden. Esto significa que solo se puede considerar un número fijo de objetos al intentar determinar si la fórmula es verdadera o falsa. Claramente, esto no está completo, pero si se encuentra un contraejemplo, entonces realmente es un contraejemplo.

La herramienta Alloy es una herramienta que permite que los modelos se describan en lógica de primer orden (aunque la sintaxis de la superficie se basa en modelos descritos relacionalmente) y utiliza la verificación de modelos acotados para encontrar soluciones. Se usa un solucionador SAT debajo del capó. Una extensión de aleación permite modelos con un carácter temporal, aunque técnicamente no es compatible con la lógica temporal.

Si desea explorar más a fondo, por ejemplo, para verificar la corrección del programa, puede consultar las herramientas de verificación del programa. Generalmente se basan en la lógica de Hoare (para razonar sobre condiciones previas y posteriores), posiblemente extendida con lógica de separación (para razonar sobre montones). Estas lógicas son generalmente indecidibles, por lo que se requiere una cierta cantidad de interacción entre el ser humano y la herramienta de verificación. Algunas herramientas de ejemplo son:

Dave Clarke
fuente
10

Después de leer su pregunta, la única forma en que pude ver y tuve el conocimiento suficiente para unir los temas fue dar un conjunto de artículos de alto nivel que se desglosan de la verificación de software y terminan tratando de unir la comprobación de modelos y la prueba de teoremas. Espero que mi comentario haya hecho eso:

Echar un vistazo a la verificación del software a continuación, la verificación formal entonces la comprobación de modelo y verificación de software formal: Comprobación del modelo y de demostración de teoremas

Dave ha dado una buena respuesta por la cual no puedo hacer más justicia a la primera parte de la pregunta que Dave, ya que también soy nuevo en esto.

Dado que esta es su primera pregunta en un sitio de SE , la razón por la que no di una respuesta sino un comentario es porque aquí una respuesta no puede ser solo un conjunto de enlaces, sino que debe dar una respuesta por escrito y usar enlaces en apoyo de la respuesta; por lo tanto, un comentario en lugar de una respuesta.

Con respecto a:

Cualquier sugerencia de libros o artículos para principiantes en este asunto es muy apreciada.

Los libros que sugeriría y usaría son:

En este momento no puedo expandirme más en la demostración de teoremas porque todavía estoy aprendiendo los pro / contras y las diferencias de cada uno, pero en los que me estoy enfocando son

  • HOL Light por el libro de John Harrison.
  • Coq porque se basa en cálculos de construcciones
  • Isabelle porque se basa en la unificación de orden superior.

    Estos asistentes de prueba también suelen tener libro (s), son actuales, populares, de código abierto, mantenidos y tienen comunidades de apoyo activas.

Nota: Usé worldcat.org para hacer referencia a los libros, pero puede revisarlos utilizando la función de mirar dentro de Amazon.

Guy Coder
fuente
Para evitar muchas ediciones en la respuesta, soltaré la información agregada como comentarios y luego en el futuro las incluiré en la respuesta. Por tratar de resolver las muchas similitudes y diferencias entre los asistentes de prueba. Google para Freek Wiedijk; Encuentro que sus documentos son bastante útiles.
Guy Coder
Muchas, muchas gracias por su detallada y completa respuesta. Para agregar sus comentarios en libros y proporcionar un enlace al libro gratuito. Nuevamente, no puedo agradecerles lo suficiente :-)
FELIPE N.