---
name: "alt-ergo"
section: "1"
platform: "linux"
package: "alt-ergo"
version: "2.0.0-7+b4"
release: "Debian 11 (Bullseye)"
platforms: ["linux"]
url: "https://new.carta.tech/alt-ergo"
---

# alt-ergo(1)

An automatic theorem prover dedicated to program verification

## NAME

Alt-Ergo - An automatic theorem prover dedicated to program verification

## SYNOPSIS

**alt-ergo** \[ **options** \] **file**

## DESCRIPTION

**Alt-Ergo** is an automatic theorem prover.  It takes as inputs an arbitrary polymorphic and multi-sorted first-order formula written is a why like syntax.

## OPTIONS

- **-h**

  Help. Will give you the full list of command line options.

## EXAMPLES

- A theory of functional arrays with integer indexes . This theory provides a built-in type ('a,'b) farray and a built-in syntax for manipulating arrays.

  For instance, given an abstract datatype tau and a functional array t of type (int, tau) farray declared as follows:

  type tau

  logic t : (int, tau) farray

  The expressions:

  t\[i\] denotes the value stored in t at index i

  t\[i1\<-v1,...,in\<-vn\] denotes an array which stores the same values as t for every index except possibly i1,...,in, where it stores value v1,...,vn. This expression is equivalent to ((t\[i1\<-v1\])\[i2\<-v2\])...\[in\<-vn\].

  Examples.

  t\[0\<-v\]\[1\<-w\]

  t\[0\<-v, 1\<-w\]

  t\[0\<-v, 1\<-w\]\[1\]

- A theory of enumeration types.

  For instance an enumeration type t with constructors A, B, C is defined as follows :

  type t = A \| B \| C

  Which means that all values of type t are equal to either A, B or C. And that all these constructors are distinct.

- A theory of polymorphic records.

  For instance a polymorphic record type 'a t with two labels a and b of type 'a and int respectively is defined as follows:

  type 'a t = { a : 'a; b : int }

  The expressions { a = 4; b = 5 } and { r with b = 3} denote records, while the dot notation r.a is used to access to labels.

- Alt-Ergo (v. \>= 0.95) allows the user to force the type of terms using the syntax \<term\> : \<type\>. The example below illustrates the use of this new feature.

  type 'a list

  logic nil : 'b list

  logic f : 'c list -\> int

  goal g1 : f(nil) = f(nil) (\* not valid because the two instances of nil may have different types \*)

  goal g2 : f(nil:'d list) = f(nil:'d list) (\* valid \*)

## ENVIRONMENT VARIABLES

- **ERGOLIB**

  Alternative path for the Alt-Ergo library

## AUTHORS

Sylvain Conchon *\<conchon@lri.fr\>* and Evelyne Contejean *\<contejea@lri.fr\>*

## SEE ALSO

Alt-Ergo web site: *http://alt-ergo.lri.fr*