Jape es un asistente gráfico de pruebas configurable , desarrollado originalmente por Richard Bornat en la Universidad Queen Mary de Londres y Bernard Sufrin en la Universidad de Oxford . [2] El programa está disponible para los sistemas operativos Mac , Unix y Windows . Está escrito en el lenguaje de programación Java y publicado bajo la licencia GNU GPL .
Se afirma que Jape es el programa más popular para la "enseñanza de lógica asistida por computadora" que implica ejercicios de desarrollo de pruebas en lógica matemática . [3]
Jape fue creado en 1992 por Richard Bornat y Bernard Sufrin con la intención de comprender mejor el razonamiento formal. Bernard Sufrin fue el creador del nombre "Jape". [2]
En 2019, publicaron el código en GitHub. [4]
Jape permite el descubrimiento de pruebas dirigido por humanos en una lógica definida por el usuario como un sistema de reglas de inferencia . Asigna los gestos del usuario (por ejemplo, escribir, hacer clic o arrastrar el ratón) a las acciones de prueba del asistente. Jape no tiene ningún conocimiento especial de ninguna lógica o teoría de objetos , y realizará movimientos en una prueba si y solo si son justificables por las reglas de la lógica de objetos que está cargada actualmente. [5] Jape permite realizar pasos de prueba y deshacerlos, y muestra el efecto de los pasos de prueba añadidos, lo que ayuda a comprender las estrategias para encontrar pruebas. [2] : 60 Cuando el usuario añade y elimina los pasos de prueba, se construye el árbol de pruebas que Jape puede mostrar en forma de árbol o en forma de caja. [5] Jape permite mostrar pruebas en diferentes niveles de abstracción. También es posible presentar una prueba hacia adelante en un estilo de deducción natural utilizando los modos especializados de visualización para pruebas. [6]
Jape trabaja con variantes del cálculo secuencial y la deducción natural . También admite pruebas formales con cuantificadores . [2] : 84