¿Existe algún asistente de pruebas basado en la lógica de primer orden?

Question

Estoy buscando un asistente de pruebas para escribir pruebas formales sobre hechos básicos de la teoría de conjuntos, como por ejemplo

• $a\subseteq a$
• $(a,b)=(c,d)\leftrightarrow a=c\land b=d$

La deducción natural para la lógica de primer orden es el único conjunto de reglas de inferencia que me gustaría utilizar. Se prefiere un software fácil de instalar y de usar a uno más complicado. También se prefiere el software de código abierto sobre el de código cerrado. No importa si el software viene con un archivo de pruebas que ya han sido formalizadas: Me gustaría empezar desde cero.

Gracias.

Answer 1

Puedes probar Doce . Se basa en una teoría de tipos dependientes más potente, pero la lógica de primer orden puede codificarse en unas pocas líneas (incluidas en el directorio de ejemplos), permitiéndole escribir pruebas de deducción natural como términos lambda. También puedes echar un vistazo a esto breve axiomatización de la teoría de conjuntos ZFC .

Answer 2

Isabelle soporta muchas lógicas diferentes, y tiene una formulación de lógica de primer orden que puedes consultar aquí: http://isabelle.in.tum.de/dist/library/FOL/index.html . Sin embargo, aunque las pruebas tienen sabor a deducción natural, no produce nada que un lógico entienda como una derivación de deducción natural tras una inspección superficial.

Los demostradores de teoremas automatizados Prover9 , E , SPASS y Vampiro son todos sistemas de primer orden. No producen pruebas utilizando la deducción natural (todos son sistemas típicamente basados en la resolución/paramodulación).

Suena como ProofWeb es exactamente lo que quieres. Proporciona un sistema para mostrar la prueba de deducción natural/calculo secuencial que la acompaña junto con una formalización asistida por ordenador. También tiene una interfaz interactiva muy agradable para los estudiantes, y ofrece la posibilidad de asignar ejercicios. Por otro lado, sé que ha sido desarrollado en gran medida para Coq, que es mucho, mucho más expresivo que la lógica de primer orden. Y aunque sé que hay un desarrollo de la teoría de conjuntos dentro de Coq, sospecho que modificar el sistema para la teoría de conjuntos básica sería un ejercicio no trivial.

Answer 3

Quizá quieras buscar el libro de John Harrison: Handbook of Practical Logic and Automated Reasoning. En el libro (entre otras cosas) desarrolla un probador de teoremas interactivo para la lógica de primer orden en OCaml. El código es disponible en línea .

EDIT: El sistema en el libro se basa en un cálculo de estilo Hilbert, pero debido al estilo LCF de la interacción, se puede hacer sentir mucho como la deducción natural.

Answer 4

Trate de Richard Bornat sistema de Jape . Es una herramienta de enseñanza con un módulo para la deducción natural, así que hay una interfaz gráfica de usuario. la automatización de la prueba es muy limitado, ya que se trata de enseñar a la gente cómo hacer las pruebas formales, pero a partir del sonido de su pregunta que suena exactamente lo que quiere.

Answer 5

El Diseñador de Pruebas de Daniel Velleman es un applet de java que escribe esquemas de pruebas en teoría elemental de conjuntos, bajo la guía del usuario. El enfoque de Proof Designer para la escritura de pruebas es similar al enfoque utilizado en su libro How to Prove it.

http://www.cs.amherst.edu/~djv/pd/pd.html