Hispanopedia Wiki
Articulo de referencia

Proverbio 9

Prover9 es un demostrador automático de teoremas para lógica de primer orden y lógica ecuacional desarrollado por William McCune . Descripción Prover9 es el sucesor del demostra...

Hispanopedia WikiContenido en espanolLectura gratuita

Prover9 es un demostrador automático de teoremas para lógica de primer orden y lógica ecuacional desarrollado por William McCune .

Descripción

Prover9 es el sucesor del demostrador de teoremas Otter , también desarrollado por William McCune . [ 1 ] : 1 Prover9 se destaca por producir demostraciones relativamente legibles y por tener una poderosa estrategia de sugerencias. [ 1 ] : 11

Prover9 se combina intencionalmente con Mace4 , que busca modelos finitos y contraejemplos. Ambos pueden ejecutarse simultáneamente a partir de la misma entrada, [ 2 ] donde Prover9 intenta encontrar una prueba, mientras que Mace4 intenta encontrar un contraejemplo (que la refute). Prover9, Mace4 y muchas otras herramientas se basan en una biblioteca subyacente llamada LADR ("Library for Automated Deduction Research") para simplificar la implementación. Las pruebas resultantes pueden ser verificadas por Ivy, una herramienta de verificación de pruebas que ha sido verificada por separado utilizando ACL2 .

En julio de 2006, el lenguaje de entrada de LADR/Prover9/Mace4 experimentó un cambio importante (que también lo diferencia de Otter). La distinción clave entre "cláusulas" y "fórmulas" desapareció por completo; ahora las "fórmulas" pueden tener variables libres , y las "cláusulas" son un subconjunto de las "fórmulas". Prover9/Mace4 también admite un tipo de fórmula "objetivo", que se niega automáticamente para la demostración. Prover9 intenta generar una demostración automáticamente por defecto; en cambio, el modo automático de Otter debe configurarse explícitamente.

Prover9 estuvo en desarrollo activo, con nuevas versiones cada mes o cada dos meses, hasta 2009. Prover9 es software libre y, por lo tanto, de código abierto ; se publica bajo la licencia GPL versión 2 o posterior. En 2026, se publicó una nueva versión llamada LADR-2026, que reescribe y amplía las capacidades tanto de Prover9 como de Mace4. [ 3 ]

Ejemplos

Sócrates

La afirmación tradicional "todos los hombres son mortales", "Sócrates es un hombre", prueba "Sócrates es mortal" puede expresarse de esta manera en Prover9:

fórmulas ( supuestos ). hombre ( x ) -> mortal ( x ). % fórmula abierta con variable libre x hombre ( socrates ). fin_de_lista .fórmulas ( objetivos ). mortal ( socrates ). fin_de_lista .

Esto se convertirá automáticamente a forma clausal (que Prover9 también acepta):

fórmulas ( sos ). - hombre ( x ) | mortal ( x ). hombre ( socrates ). - mortal ( socrates ). fin_de_lista .

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: [ 4 ]

fórmulas ( suposiciones ). 1 * x = x . % identidad x * y = y * x . % conmutatividad x * ( y * z ) = ( x * y ) * z . % asociatividad ( x * y = x * z ) -> y = z . % cancelación (0 no está permitido, por lo que x!=0). % % Ahora definamos divide(x,y): x divide a y. % Ejemplo: divide(2,6) es verdadero porque 2*3=6. % divide ( x , y ) <-> ( existe z x * z = y ). divide ( 2 , x * x ) -> divide ( 2 , x ). % Si 2 divide a x*x, divide a x. a * a = 2 * ( b * b ). % a/b = sqrt(2), por lo que a^2 = 2 * b^2. ( x ! = 1 ) -> - ( divide ( x , a ) & divide ( x , b )). % a/b está en términos mínimos 2 ! = 1. % El autor original casi olvidó esto. fin_de_lista .

Referencias

  1. 1 2 Phillips, JD; Stanovsky, David. "Demostración automatizada de teoremas en la teoría de bucles" (PDF) . Universidad Charles . Archivado (PDF) del original el 28 de marzo de 2018. Recuperado el 15 de noviembre de 2018 .
  2. ↑ Berghammer, Rudolf; Struth, Georg (21 de junio de 2010). «Sobre la construcción y verificación automatizada de programas» (PDF) . En Bolduc, Claude; Desharnais, Jules; Ktari, Bechir (eds.). Matemáticas de la construcción de programas, Actas . 10.ª Conferencia Internacional, MPC 2010. Ciudad de Quebec . doi : 10.1007/978-3-642-13321-3 . ISBN 978-3-642-13320-6. S2CID 6962311 . Archivado del original (PDF) el 19 de noviembre de 2018 . Recuperado el 19 de noviembre de 2018 . 
  3. ↑ Machado, J.; Lesyna, L. (2026). "LADR-2026 mejorado" . Recuperado el 23 de marzo de 2026 .
  4. ↑ Wheeler, David A. "sqrt2.in" . Página web personal de David A. Wheeler . Consultado el 14 de marzo de 2016 .
  • Página principal de Prover9
  • Página principal de Old Prover9
  • Prover9 – Mace4 – Foros LADR
  • Métodos formales (ejemplo de raíz cuadrada de 2)