UNIVERSITY OF BELGRADE
DEPARTMENT FOR COMPUTER SCIENCE

ARGO

Automated reasoning group

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