Prover9 es un demostrador automatizado de teoremas para lógica de primer orden y ecuaciones desarrollado por William McCune .
Descripción
Prover9 es el sucesor del demostrador del teorema de Otter también desarrollado por William McCune . [1] : 1 Prover9 se destaca por producir pruebas relativamente legibles y tener una poderosa estrategia de pistas. [1] : 11
Prover9 se empareja intencionalmente con Mace4 , que busca modelos finitos y contraejemplos. Ambos pueden ejecutarse simultáneamente desde la misma entrada, [2] con Prover9 intentando encontrar una prueba, mientras que Mace4 intenta encontrar un contraejemplo (refutación). Prover9, Mace4 y muchas otras herramientas se basan en una biblioteca subyacente llamada LADR ("Biblioteca para investigación de deducción automatizada") para simplificar la implementación. Ivy, una herramienta de verificación de pruebas que se ha verificado por separado mediante ACL2, puede verificar las pruebas resultantes .
En julio de 2006, el lenguaje de entrada LADR / Prover9 / Mace4 realizó un cambio importante (que también lo diferencia de Otter). La distinción clave entre "cláusulas" y "fórmulas" desapareció por completo; Las "fórmulas" ahora pueden tener variables libres ; y las "cláusulas" son ahora un subconjunto de "fórmulas". Prover9 / Mace4 también admite un tipo de fórmula de "objetivo", que se niega automáticamente como prueba. Prover9 intenta generar automáticamente una prueba de forma predeterminada; por el contrario, el modo automático de Otter debe establecerse explícitamente.
Prover9 estuvo en desarrollo activo, con nuevos lanzamientos cada mes o cada dos meses, hasta 2009. Prover9 es software libre y, por lo tanto, software de código abierto ; se publica bajo GPL versión 2 o posterior.
Ejemplos de
Sócrates
El tradicional "todos los hombres son mortales", "Sócrates es un hombre", prueba que "Sócrates es mortal" se puede expresar de esta manera en Prover9:
fórmulas (supuestos). hombre (x) -> mortal (x). % fórmula abierta con variable libre x hombre (sócrates).end_of_list.
fórmulas (metas). mortal (sócrates).end_of_list.
Esto se convertirá automáticamente en forma clausal (que Prover9 también acepta):
fórmulas (sos). -hombre (x) | mortal (x). hombre (sócrates). -mortal (sócrates).end_of_list.
La raíz cuadrada de 2 es irracional
Una prueba de que la raíz cuadrada de 2 es irracional se puede expresar de esta manera: [3]
fórmulas (supuestos). 1 * x = x. % identidad x * y = y * x. % conmutatividad x * (y * z) = (x * y) * z. % asociatividad (x * y = x * z) -> y = z. % de cancelación (0 no está permitido, entonces x! = 0). % % Ahora definamos divide (x, y): x divide y. % Ejemplo: divide (2,6) es cierto porque 2 * 3 = 6. % divide (x, y) <-> (existe zx * z = y). divide (2, x * x) -> divide (2, x). % Si 2 divide x * x, divide x. a * a = 2 * (b * b). % a / b = sqrt (2), entonces a ^ 2 = 2 * b ^ 2. (x! = 1) -> - (divide (x, a) y divide (x, b)). % a / b está en los términos más bajos 2! = 1.% El autor original casi lo olvida.end_of_list.
Referencias
- ^ a b Phillips, JD; Stanovsky, David. "Demostración automatizada de teoremas en teoría de bucles" (PDF) . Universidad Charles . Archivado (PDF) desde el original el 28 de marzo de 2018 . Consultado el 15 de noviembre de 2018 .
- ^ Berghammer, Rudolf; Struth, Georg (21 de junio de 2010). "Sobre la construcción y verificación de programas automatizados" (PDF) . En Bolduc, Claude; Desharnais, Jules; Ktari, Bechir (eds.). Matemáticas de la construcción del programa, Actas . X Conferencia Internacional, MPC 2010. Ciudad de Quebec . doi : 10.1007 / 978-3-642-13321-3 . ISBN 978-3-642-13320-6. Archivado desde el original (PDF) el 19 de noviembre de 2018 . Consultado el 19 de noviembre de 2018 .
- ^ Wheeler, David A. "sqrt2.in" . Página de inicio personal de David A. Wheeler . Consultado el 14 de marzo de 2016 .