Downloads
Formalisations
Faradžev/Read type isomorph-free generation
Isabelle/HOL formalization
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