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.
Respuestas:
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:
fuente
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:
Los libros que sugeriría y usaría son:
Lógica en Ciencias de la Computación - Modelado y razonamiento sobre sistemas 2nd Ed. por Huth y Ryan Esto introduce la lógica y sube a la verificación del modelo, pero no entra en la prueba del teorema. Por lo tanto, esto debería cubrir todas sus preguntas básicas relacionadas con la lógica y la verificación de modelos.
Principios de verificación de modelos por Baier y Katoen Acabo de empezar a leer este, y es mucho mejor que leer muchos documentos y tratar de ver cómo encajan. Este es uno de los libros más, si no el más recomendado, sobre el tema de la verificación de modelos. Debería responder a sus preguntas más avanzadas sobre la verificación de modelos.
Lógica temporal y sistemas de estado de Kroger y Merz A menudo me gusta tener libros de diferentes autores cuando uno mismo aprende por sí mismo. Éste es para complementar / completar los "Principios de verificación de modelos"
Manual de lógica práctica y razonamiento automatizado por Harrison Como programador, no puedo recomendar este libro lo suficiente. El libro comienza con la introducción de la lógica y avanza hasta el punto de crear el núcleo para un probador de teoremas basado en el trabajo de HOL Light . Solo para resaltar que el libro usa el código OCaml en funcionamiento, explica los teoremas en términos que considero amigables y le brinda lo que necesita saber, pero no tanto que no pueda hacer la conexión o sienta que está corriendo por las vías laterales. If es un libro muy enfocado en pasar de la lógica a un tipo específico de demostrador de teoremas.
Cómo probarlo: un enfoque estructurado de Velleman Para entrar en los asistentes de prueba para demostrar el teorema, necesitará vivir y dormir teoremas.
Una introducción a las pruebas y la lengua vernácula matemática por día Este es un libro gratuito que no solo complementa "Cómo probarlo", sino que va más allá en suma. No me sorprendería ver que este se haga popular.
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
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.
fuente