Solving First-Order Constraints over the Monadic Class. - Dimitri Chubarov; Andrei Voronkov (Mechanizing Mathematical Reasoning, 2005)

Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications. - Dimitri Chubarov; Andrei Voronkov (MFCS, 2005)