Read a statement on standard input and display its proof on standard output.
-h, --help
display this help and exit
-v, --version
output version information and exit
-d, --debug
print debug information while gappa is running
Engineparameters:-Eprecision=int
internal precision (default: 60)
-Edichotomy=int
dichotomy depth (default: 100)
-E[no-]reverted-fma
change fma(a,b,c) from a*b+c to c+a*b
-Echange-threshold=float
threshold for new results (default: 0.01)
-Eno-auto-dichotomy
do not choose a term for automatic splitting
Enginemodes:-Munconstrained
do not check for theorem constraints
-Mstatistics
display statistics
-Mschemes[=FILE]
produce a dot graph (default: schemes.dot)
Warnings: (default: all)
-W[no-]dichotomy-failure-W[no-]hint-difference-W[no-]null-denominator-W[no-]unbound-variableBackend:-Bnull do not generate a proof (default)
-Bcoq produce a script for Coq
-Bcoq-lambda
produce a lambda-term for Coq
-Bholl produce a script for HOL Light
-Blatex
produce a LaTeX text
-Bd2 produce a D2 graph file
Gappa 1.5.0 January 2025 GAPPA(1)