## Downloads

### Formalisations

Erdős-Szekeres conjecture

KRK chess endgame

Complex geometry

Classic DPLL procedure

Modern SAT solver verification

Frankl's Conjecture: FC Families

Simplex procedure

Tarski's book

Automated verification of high school geometry

Automated verification of informal proofs

### Software

**ArgoSat**

Source code (v1.0)

**ArgoSmArT (solver portfolio)**

Source and binaries

**ArgoSmArT k-NN**

Source and binaries

**ArgoLib**

Description for SMTCOMP'07

Source code (v3.5)

Binary for linux (v3.5)

**ArgoClp**

Executable (v2.0)

Executable (v3.0) (with automated support for dealing with symmetric predicates and reformulations of lemmas)

Executable (v4.0) (with support for tptp input and XML output)

**GCLC - geometry software**

Distribution

**LAV**

LAV page

**Non-CNF instance features computation**

Source
code and executables

**OpenGeoProver - Wu's method for geometry theorem proving**

Source code

**A strategy for KRK Chess endgame**

URSA specifications (of the game,
strategy, and correctness lemmas) and C program for analysis of KRK

**meSAT**

meSAT page (instance based selection of encodings included)

**ATCo shift scheduling**

ATCo shift scheduling page

**Sudoku solver and generator**

Sudoku page

**Coherent logic Vernacular**

CLVernacular

**ArgoTriCS - Triangle Construction Solver**

ArgoTriCS

**Marc Bezem's **
CL (Coherent Logic) page on Hessenberg's Theorem