¿Cómo funcionan los verificadores de pruebas?

Question

Actualmente estoy tratando de entender los conceptos y la teoría que hay detrás de algunos de los verificadores de pruebas más comunes que existen, pero no estoy muy seguro de la naturaleza exacta y la construcción del tipo de sistemas / cálculos de pruebas que utilizan. ¿Se basan esencialmente en lógicas de orden superior que utilizan la semántica de Henkin, o hay algo más? Según tengo entendido, extender la semántica de Henkin a la lógica de orden superior no hace que el sistema formal sea menos sólido, aunque no lo tengo muy claro.

Aunque principalmente estoy buscando una respuesta general con ejemplos útiles, aquí hay algunas preguntas específicas:

• ¿Cuál es exactamente el papel de la teoría de tipos en la creación de lógicas de orden superior? Lo mismo ocurre con la teoría de categorías/teoría de modelos, que creo que es una alternativa.
• ¿Es la extensión de a) la deducción natural, b) el cálculo secuencial, o c) algún otro sistema formal la mejor manera de crear lógicas de orden superior?
• ¿Dónde entra el cálculo lambda tipificado en la verificación de pruebas?
• ¿Existen otros enfoques, además de la lógica de orden superior, para la verificación de pruebas?
• ¿Cuáles son las limitaciones/deficiencias de los sistemas de verificación de pruebas existentes (véase más abajo)?

Las páginas de Wikipedia sobre programas de verificación de pruebas como Luz HOL Coq y Metamath dan alguna idea, pero estas páginas contienen información limitada y poco clara, y hay muy pocos recursos específicos de alto nivel en otros lugares. Hay tantas variaciones en la lógica formal/sistemas utilizados en la teoría de la prueba que no estoy seguro de cuáles son las ideas básicas de estos sistemas - lo que es necesario u óptimo y lo que está abierto a la experimentación.

Tal vez una buena manera de responder a esto, ciertamente una que yo apreciaría, sería una breve guía (aunque con algunos detalles técnicos/específicos) sobre cómo se podría generar un cálculo de pruebas completo (sistema de verificación de pruebas) desde cero. Sin embargo, cualquier otra información en forma de explicaciones y ejemplos también sería estupenda.

Answer 1

Responderé sólo a una parte de su pregunta: Creo que las otras partes se aclararán a partir de esto.

Un verificador de pruebas es esencialmente un programa que toma un argumento, una representación de la prueba, y comprueba que ésta está correctamente construida, y dice OK si lo está, y falla silenciosamente en caso contrario, o destaca lo que no es válido en caso contrario.

En principio, la representación de la prueba podría ser simplemente una secuencia de fórmulas en un sistema de Hilbert: todas las lógicas (al menos, las lógicas de primer orden) pueden representarse de esta manera. Ni siquiera es necesario decir qué regla se especifica en cada paso, ya que es decidible si cualquier fórmula se sigue por una aplicación de regla a partir de fórmulas anteriores.

En la práctica, sin embargo, las representaciones de las pruebas son más complejas. Metamath se acerca bastante a los sistemas de Hilbert, pero tiene un rico conjunto de reglas. Coq y LF utilizan cálculos lambda tipados (diferentes) con definiciones para representar los pasos, que son computacionalmente bastante caros de comprobar (IIRC, ambos son difíciles de PSPACE). Y el verificador de pruebas puede hacer mucho más: Coq permite extraer programas ML de las pruebas.

Answer 2

No creo que la gente que trabaja en la demostración de teoremas de orden superior se preocupe realmente de la semántica de Henkin o de los modelos en general, sino que trabajan principalmente con sus cálculos de demostración. Mientras no haya contradicciones u otros teoremas contraintuitivos, están contentos. El teorema más importante y más difícil que demuestran suele ser que sus términos de prueba terminan, lo que, según creo, puede considerarse una forma de solidez.

La semántica de Henkin es más interesante para la gente que intenta extender sus métodos de primer orden a la lógica de orden superior, porque se comporta esencialmente como modelos de la lógica de primer orden. La semántica de Henkin es algo más débil que lo que se obtendría con la semántica teórica de conjuntos estándar, que por el teorema de incompletitud de Gödels no puede tener un cálculo de prueba completo. Creo que las teorías de tipos deberían estar en algún lugar entre la semántica de Henkin y la estándar.

¿Dónde entra el cálculo lambda tipificado en la verificación de pruebas?

Para demostrar alguna implicación P(x) --> Q(x) con algunas variables libres x necesitas mapear cualquier prueba de P(x) a una prueba de Q(x) . Sintácticamente, un mapa (una función) puede representarse como un término lambda.

¿Existen otros enfoques, además de la lógica de orden superior, para la verificación de pruebas?

También se pueden verificar las pruebas en la lógica de primer orden o en cualquier otra, pero entonces se perdería gran parte de la potencia de la lógica. La lógica de primer orden es sobre todo interesante porque es posible encontrar automáticamente pruebas, si no son demasiado complicadas. Lo mismo ocurre con la lógica proposicional.

¿Cuáles son las limitaciones/deficiencias de los sistemas de verificación de pruebas existentes (véase más abajo)?

Cuanto más potente es la lógica, más difícil es construir pruebas.

Dado que los sistemas están disponibles de forma gratuita, le sugiero que juegue con ellos, por ejemplo, con Isabelle y Coq para empezar.

Answer 3

ML y similares fueron diseñados como (meta) lenguajes de programación para soportar la creación de encadenamientos y tácticas hacia atrás. Pero la verificación de pruebas es encadenamiento hacia delante y es una tarea bastante trivial asumiendo que la prueba ya se ha presentado formalmente, ya que la formalización y la verificabilidad mecánica verificabilidad son generalmente pleonásticos.

En el más simple se puede hacer con Prolog. He aquí un ejemplo. Supongamos que que estás trabajando con un sistema de deducción basado en secuencias secuencias. Y tienes las siguientes dos reglas de inferencia:

 -------- (id)
 A |- A

 G |- forall x: A(x)
 ------------------- (inst)
 G |- A(t)

Entonces puede codificar estas reglas como predicados de Prolog de la siguiente manera:

% id(+Prop, -Seq)
id(A,(A :- A)).

% inst(+Seq, +Term, -Seq)
inst((G :- forall(X^A)), T, (G :- B)) :- call(X^(A=B),T).

Ahora supongamos que quieres verificar la siguiente prueba:

--------------------------------- (Id)
forall x: p(x) |- forall x : p(x)
--------------------------------- (inst)
forall x: p(x) |- p(a)

A continuación, basta con ejecutar la siguiente consulta Prolog:

?- id(forall(X^p(X)),S), inst(S,a,R).
R = (forall(X^p(X)) :- p(a)).

Una razón para utilizar tipos aquí sería su capacidad para modelar los teoremas probados y que su construcción imita la construcción de la prueba.

Aquí no usamos tipos, por lo que tuvimos que amueblar manualmente el parámetros de la prueba, es decir, forall(X^p(X)) para el predicado id y a para el predicado inst en el ejemplo anterior.

Pero los tipos y su construcción le darían una integral representación que también sería muy susceptible a Prolog, pero no lo he mostrado aquí.

Adiós

P.D.: Lo anterior supone algunos predicados de orden superior del sistema, concretamente call/2 y ^/3. Mientras tanto, muchos sistemas Prolog tienen call/2, pero es posible que tengas que definir ^/3 por ti mismo.

Puedes hacerlo de la siguiente manera:

^(X,A,Y) :- term_variables(A,L), remove_variable(L,X,R),
    copy_term(R-X-A,R-Y-B), call(B).

remove_variable([],_,[]).
remove_variable([X|Y],Z,Y) :- X==Z, !.
remove_variable([X|Y],Z,[X|T]) :- remove_variable(Y,Z,T).

Lo anterior es válido siempre que T no sea de orden superior, y siempre que siempre que se utilicen variables separadas que sean también distintas de las variables globalmente libres.

También hace uso de term_variables/2 que es más o menos estándar ahora en muchos sistemas Prolog. Para más información sobre call/2 y term_variables/2 ver por ejemplo: http://www.complang.tuwien.ac.at/ulrich/iso-prolog/dtc2