====== Verschiedene Theorem-Beweiser ======

===== Z3 =====

Z3 ist ein SMT-Löser, d.h. er kann SAT-Formeln bezüglich verschiedener
Theorien lösen. Als Eingabesprache verwendet Z3 den
[[http://www.smtlib.org/ | SMT-LIB 2.0 standard]].

  * Installiert von [[https://github.com/Z3Prover/z3]]
  * Aufruf: ''/opt/provers/z3/bin/z3''
  * Version: 4.4.2
  * Dokumentation: [[http://rise4fun.com/Z3/tutorial/guide | Tutorial]]

===== CVC4 =====

  * Installiert von [[http://cvc4.cs.nyu.edu/downloads/]]
  * Aufruf: ''/opt/provers/cvc4/bin/cvc4''
  * Version: 1.4
  * Dokumentation: [[http://cvc4.cs.nyu.edu/wiki/User_Manual]]
  * Tutorials: [[http://church.cims.nyu.edu/wiki/Tutorials]]

==== Features ====

  * arbeitet auf einer Variante der Prädikatenlogik 1. Stufe mit polymorphen Typen
  * bereitgestellte Theorien: Lineare Arithmetik auf rationalen und Integerzahlen, Arrays, Tupel, Records, induktive Datentypen, Bitvektoren
  * Quantoren
  * interaktives Text-basiertes Interface
  * C++ API
  * Modell-Generierung

==== Installation ====

  * Entpacken des Archivs (Source tarball)
  * libantlr3c installieren: über das bereitgestelle Skript ''contrib/get-antlr-3.4''
  * Konfigurieren ''./configure --prefix <Zielpfad>''
  * Bauen mittels ''make'' und im Zielverzeichnis installieren ''make install''

===== Yices =====

  * Installiert von [[http://yices.csl.sri.com/cgi-bin/yices2-newnewlicense.cgi?file=yices-2.4.2-x86_64-unknown-linux-gnu-static-gmp.tar.gz]]
  * Aufrufe:
      * ''/opt/provers/yices/bin/yices'' (Yices-Sprache)
      * ''/opt/provers/yices/bin/yices-smt'' (SMT-LIB 1.0)
      * ''/opt/provers/yices/bin/yices-smt2'' (SMT-LIB 2.0)
      * ''/opt/provers/yices/bin/yices-sat'' (DIMACS-Format)
  * Version: 2.4.2
  * Dokumentation: [[http://yices.csl.sri.com/yices2-documentation.html]] (verschiedene Veröffentlichungen und das [[http://yices.csl.sri.com/papers/manual.pdf | Yices manual]])

==== Features ====

  * bereitgestellte Theorien: Uninterpretierte Funktionssymbole, lineare Arithmetik über reellen und Integerzahlen, Bitvektoren, skalare Typen und Tupel
  * Solver für vier verschiedene Eingabeformate
      * Yices-Spezifikationssprache 
      * SMT-LIB 1.0
      * SMT-LIB 2.0
      * DIMACS

==== Installation ====

  * Archiv entpacken
  * Installationsskript ''./install-yices <Installationsverzeichnis>'' ausführen

===== MathSAT5 =====

  * Installiert von [[http://mathsat.fbk.eu/download.html]]
  * Aufruf: ''/opt/provers/mathsat/bin/mathsat''
  * Version: 5.3.10
  * Dokumentation: [[http://mathsat.fbk.eu/documentation.html]]

==== Features ====

  * bereitgestellte Theorien: Uninterpretierte Funktionssymbole, lineare Arithmetik, Bitvektoren, Arrays
  * Modell- und Beweis-Generierung
  * inkrementelle Arbeitsweise

==== Installation ====

  * Archiv entpacken
  * Inhalte ins Zielverzeichnis kopieren