Рассмотрены различные системы аргументации и приведены результаты их сравнительного анализа. Описана процедура доказательства Какаса и Тони для аргументационной семантики допустимости, приемлемости и фундированных моделей. Выполнена программная реализация этой процедуры и рассмотрен пример ее применения для организации абдуктивного вывода.