- Главная
- Разное
- Бизнес и предпринимательство
- Образование
- Развлечения
- Государство
- Спорт
- Графика
- Культурология
- Еда и кулинария
- Лингвистика
- Религиоведение
- Черчение
- Физкультура
- ИЗО
- Психология
- Социология
- Английский язык
- Астрономия
- Алгебра
- Биология
- География
- Геометрия
- Детские презентации
- Информатика
- История
- Литература
- Маркетинг
- Математика
- Медицина
- Менеджмент
- Музыка
- МХК
- Немецкий язык
- ОБЖ
- Обществознание
- Окружающий мир
- Педагогика
- Русский язык
- Технология
- Физика
- Философия
- Химия
- Шаблоны, картинки для презентаций
- Экология
- Экономика
- Юриспруденция
Что такое findslide.org?
FindSlide.org - это сайт презентаций, докладов, шаблонов в формате PowerPoint.
Обратная связь
Email: Нажмите что бы посмотреть
Презентация на тему Системы компьютерной алгебры. Maple, mathematica, derive
Содержание
- 2. UMS (Универсальный математическийрешатель, объединение «Северный очаг», С.-Петербург,http://www.umsolver.com)
- 3. Логическая система Искра (мех.-мат МГУ, кафедра Математической теории интеллектуальных систем, проф. Подколзин А.С., http://intsys.msu.ru)
- 4. из статьи Seq_2.miztheorem Th19: seq is convergent
- 5. then A5: 0
- 6. Скачать презентацию
- 7. Похожие презентации
UMS (Универсальный математическийрешатель, объединение «Северный очаг», С.-Петербург,http://www.umsolver.com)
Слайд 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
proofassume 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; Mizar
take g=g1+g2;
let p; assume
0
Библиотека: около 1000 статей, десятки тысяч теорем, около 150 авторов
http://mizar.org
Слайд 5
then A5: 0
n1 such that
A6: for m st n1
by A3;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;
