Системы компьютерной алгебры. Maple, mathematica, derive

Сентябрь 14, 2022

Главная
Математика
Системы компьютерной алгебры. Maple, mathematica, derive

Содержание

2. UMS (Универсальный математический решатель, объединение «Северный очаг», С.-Петербург, http://www.umsolver.com)
3. Логическая система Искра (мех.-мат МГУ, кафедра Математической теории интеллектуальных систем, проф. Подколзин А.С., http://intsys.msu.ru)
4. из статьи Seq_2.miz theorem Th19: seq is convergent & seq' is convergent implies seq + seq'
5. then A5: 0 then consider n1 such that A6: for m st n1 consider n2 such
7. Скачать презентацию

Слайд 2

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

Слайд 3

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

Подколзин А.С., http://intsys.msu.ru)

Слайд 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

by A1,Def6;
consider g2 such that
A4: for p st 0

by A2,Def6;
take g=g1+g2;
let p; assume
0

Mizar
Библиотека: около 1000 статей, десятки тысяч теорем, около 150 авторов
http://mizar.org

Слайд 5

then A5: 0
then consider n1 such that
A6: for

m st n1<=m holds abs(seq.m-g1)

consider n2 such that
A7: for m st n2<=m holds abs(seq'.m-g2)

take k=n1+n2;
let m such that
A8: k<=m;
n1<=n1+n2 by NAT_1:37;
then n1<=m by A8,XREAL_1:2;
then A9: abs(seq.m-g1)

n2<=k by NAT_1:37;
then n2<=m by A8,XREAL_1:2;
then abs(seq'.m-g2)

then A10: abs(seq.m-g1)+abs(seq'.m-g2)

A11: abs((seq+seq').m-g)=abs(seq.m+seq'.m-(g1+g2)) by SEQ_1:11
.=abs(seq.m-g1+(seq'.m-g2));
abs(seq.m-g1+(seq'.m-g2))<=abs(seq.m-g1)+abs(seq'.m-g2) by COMPLEX1:142;
hence abs((seq+seq').m-g)

end;