1. Системы компьютерной алгебры Maple Mathematica Derive 2. Решатели UMS (Универсальный математический решатель, объединение «Северный очаг», С.-Петербург) - презентация

1 1. Системы компьютерной алгебры Maple Mathematica Derive 2. Решатели UMS (Универсальный математический решатель, объединение «Северный очаг», С.-Петербург) Логическая система Искра (мех.-мат МГУ, кафедра Математической теории интеллектуальных систем, проф. Подколзин А.С.) 3. Proof assistants Coq (Франция) Isabelle (Великобритания) Mizar (Польша)

2 UMS (Универсальный математический решатель, объединение «Северный очаг», С.-Петербург, )

3 Логическая система Искра (мех.-мат МГУ, кафедра Математической теории интеллектуальных систем, проф. Подколзин А.С., )

4 из статьи Seq_2.miz theorem Th19: seq is convergent & seq' is convergent implies seq + seq' is convergent proof assume that A1: seq is convergent and A2: seq' is convergent; consider g1 such that A3: for p st 0

5 then A5: 0

6 средство для творческого изучения математического анализа, объединяет свойства обучающей программы и proof assistant; Отличия от proof assistant : – простой язык – интерфейс пользователя (поле доказательства) – разработано в МФТИ Теормат