Skip to content
Sections
>> Trisquel >> Balíky >> etiona >> math >> alt-ergo
etiona  ] [  nabia  ] [  aramo  ]
[ Zdroj: alt-ergo  ]

Balík: alt-ergo (1.30+dfsg1-1)

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.

Ostatné balíky súvisiace s balíkom alt-ergo

  • závisí
  • odporúča
  • navrhuje
  • dep: libc6 (>= 2.17)
    GNU C Library: Shared libraries
    tiež virtuálny balík poskytovaný balíkom libc6-udeb
  • dep: libgdk-pixbuf2.0-0 (>= 2.22.0)
    GDK Pixbuf library
  • dep: libglib2.0-0 (>= 2.35.9)
    GLib library of C routines
  • dep: libgmp10
    Multiprecision arithmetic library
  • dep: libgtk2.0-0 (>= 2.24.31)
    GTK+ graphical user interface library
  • dep: libgtksourceview2.0-0 (>= 2.10.0)
    shared libraries for the GTK+ syntax highlighting widget
  • dep: libpango-1.0-0 (>= 1.14.0)
    Layout and rendering of internationalized text
  • dep: zlib1g (>= 1:1.1.4)
    compression library - runtime
  • sug: why
    Software verification tool for C and Java

Stiahnuť alt-ergo

Stiahnuť pre všetky dostupné architektúry
Architektúra Veľkosť balíka Nainštalovaná veľkosť Súbory
i386 2,433.3 kB13327 kB [zoznam súborov]