---
name: "gappa"
section: "1"
platform: "linux"
package: "gappa"
version: "1.6.0-1"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/gappa"
---

# gappa(1)

manual page for Gappa 1.6.0

## NAME

Gappa - manual page for Gappa 1.6.0

## SYNOPSIS

**gappa** \[*OPTIONS*\] \[*FILE*\]

## DESCRIPTION

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

### Engine parameters:

- **-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

### Engine modes:

- **-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-variable**

### Backend:

- **-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