Cuando se especifica una fórmula en Z3 unsat y (get-proof) hay un resultado que no encuentro ninguna información acerca de lo que es. ¿Dónde puedo encontrar documentación sobre eso?Salida de contraejemplo de Z3
Me parece bastante ilegible, ¿hay alguna herramienta que lo tome como entrada?
Cheers, Matt
Las "pruebas" producidas por Z3 no son para el consumo humano. Se describe una versión obsoleta del formato en el documento: Proofs and Refutations, and Z3. El archivo z3_api.h tiene una descripción larga de cada una de las reglas de prueba. Los identificadores de la regla de prueba comienzan con Z3_OP_PR. Conozco dos aplicaciones que usan los objetos de prueba Z3. Los siguientes documentos contienen muchos ejemplos y describen cómo se pueden usar los objetos de prueba.
1- Isabelle Interactive Theorem Prover: las pruebas Z3 se reconstruyen dentro de Isabelle usando un núcleo de confianza. Usted puede encontrar varios artículos que describen este trabajo y el formato de la prueba Z3 en Sascha Bohme's homepage
Como dicha almohadilla, unsat-cores son mucho más fáciles de usar.
Muchas gracias por sus enlaces. Echaré un vistazo a ambos métodos. ¡Así que también gracias a @pad! – MattKay
El comando '(get-unsat-core)' parece ser lo que desea. Ejemplo oficial: http://rise4fun.com/Z3/smtc_core – pad