## Downloads

### Formalisations

**A strategy for KRK Chess endgame**

URSA specifications, C program for analysis, and Isabelle/HOL formalization of KRK, submitted, 2018.

URSA specifications and C program for analysis of KRK, ICGA Journal, 2013.

**Erdős-Szekeres conjecture**

Isabelle/HOL formalization for hexagons

**Frankl's conjecture**

Frankl's Conjecture: Full classification of FC(6) families, Statistics

Frankl's Conjecture: FC Families, Calculemus, 2012.

**SAT/SMT verification**

Classic DPLL procedure

Modern SAT solver verification

Simplex procedure

**Geometry**

Poincare disc model of hyperbolic geometry

Complex geometry

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)

**ArgoChecker**

ArgoChecker page

**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

**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

**Touch&Drag **

GooglePlay application

**ArgoTriCS corpus of problems for Portfolio approach **

Corpus of problems