# “alt-ergo” 0.95.1-2 source package in Ubuntu

## Changelog

alt-ergo (0.95.1-2) unstable; urgency=low * upload to unstable -- Ralf Treinen <email address hidden> Fri, 10 May 2013 21:19:12 +0200

## Upload details

- Uploaded by:
- Debian OCaml Maintainers on 2013-05-11

- Uploaded to:
- Sid

- Original maintainer:
- Debian OCaml Maintainers

- Component:
- main

- Architectures:
- any

- Section:
- math

- Urgency:
- Low Urgency

## See full publishing history Publishing

Series | Published | Component | Section |
---|

## Downloads

File | Size | MD5 Checksum |
---|---|---|

alt-ergo_0.95.1-2.dsc | 1.5 KiB | d144edc8ed5aa72d8c058862d0748930 |

alt-ergo_0.95.1.orig.tar.gz | 233.5 KiB | c0f1cbfdae04f1c37853ed5fd10154ec |

alt-ergo_0.95.1-2.debian.tar.gz | 14.0 KiB | 7e4b62f2ee85e1bb15bf2258236dd1bb |

### Available diffs

- diff from 0.94-2 to 0.95.1-2 (155.0 KiB)

## Binary packages built by this source

- alt-ergo: Automatic theorem prover dedicated to program verification
Alt-Ergo is an automatic theorem prover geared towards application in

program verification. It is based on CC(X), a congruence closure

algorithm parameterized by an equational theory X. Alt-Ergo has

built-in provers for propositional logic, linear arithmetic,

uninterpreted function symbols, associative-commutative function

symbols, polymorphic arrays, user-defined polymorphic record types

and polymorphic enumeration types. It has restricted support for

reasoning over arbitrary user-defined algebraic types, first-order

quantifiers, and non-linear arithmetic.

.

This package contains the prover as a command-line executable

as well as the graphical interface.

- libalt-ergo-ocaml-dev: Theorem prover dedicated to program verification - libraries
Alt-Ergo is an automatic theorem prover geared towards application in

program verification. It is based on CC(X), a congruence closure

algorithm parameterized by an equational theory X. Alt-Ergo has

built-in provers for propositional logic, linear arithmetic,

uninterpreted function symbols, associative-commutative function

symbols, polymorphic arrays, user-defined polymorphic record types

and polymorphic enumeration types. It has restricted support for

reasoning over arbitrary user-defined algebraic types, first-order

quantifiers, and non-linear arithmetic.

.

This package contains the development libraries that are useful when

writing OCaml programs linking to the alt-ergo API.