Анотація. Відображено результати випробувань інструментів спрощення формул, а також описано алгоритм побудови канонічних форм лінійних напівалгебраїчних формул (ЛНФ). Основним результатом цієї роботи є визначення канонічної форми ЛНФ з властивістю унікальності та іншими корисними властивостями, а також опис алгоритму її побудови .
Ключові слова: системи лінійних нерівностей, алгебраїчне програмування, верифікація програмного забезпечення, канонічні форми, лінійні напівалгебраїчні формули.
Львов Михаил Сергеевич,
доктор физ.-мат. наук, профессор, заведующий кафедрой Херсонского государственного университета, lvov@ksu.ks.ua
Песчаненко Владимир Сергеевич,
доктор физ.-мат. наук, доцент, профессор кафедры Херсонского государственного университета, vladim@ksu.ks.ua
Летичевский Александр Александрович,
доктор физ.-мат. наук, старший научный сотрудник Института кибернетики им. В.М. Глушкова
НАН Украины, Киев, lit@iss.org.ua
Тарасич Юлия Геннадиевна,
аспирантка Херсонского государственного университета, yutarasich@ksu.ks.ua, yutarasich@gmail.com
Баев Андрей Святославович,
студент Херсонского государственного университета, andreybayev95@gmail.com