Математика

Prover9 является автоматическим построителем доказательства теорем для логики первого порядка и эквациональной логики. В нем используются методы вывода упорядоченных резолюций и парамодуляций с буквальным выбором.

Сайт разработчика: http://www.cs.unm.edu/~mccune/mace4/
Что почитать?

• Пруверство для дебилов

OTTER - программа автоматического доказательства теорем

Сайт разработчика: http://www.cs.unm.edu/~mccune/otter/
Что почитать?

• Множество поддержки
• Средства автоматического доказательства теорем
• LeanCOP: Доказатель теорем, основанный на методе связей

Пакет MCL - это реализация алгоритма кластеризации Маркова (Markov Cluster algorithm), содержащий утилиты для манипуляций с разреженными матрицами и проведения кластерных экспериментов.

Сайт разработчика: http://micans.org/mcl/

Matita (по итальянски это значит карандаш) - это экспериментальная интерактивная система проверки теорем, разрабатываемая департаментом компьютерных наук (

Сайт разработчика: http://matita.cs.unibo.it/

GiNaC - мощная библиотека для различных математический вычислений на C++ с удобным api. Для чисел использует длинную арифметику CLN(Common Lisp Numbers), способна решать различные ДУ, и нелинейные уравнения.

Тип приложения: библиотека
Сайт разработчика: http://www.ginac.de/
Что почитать?

• GiNaC (C++)
• GiNaC 1.6.0 - C++ библиотека для символьных вычислений
• Новый выпуск 1.6.0 C++ библиотеки GiNaC

Lybniz - это простая программа для построения графиков математических функций.

Тип приложения: графические программы на основе библиотеки GTK
Сайт разработчика: http://lybniz2.sourceforge.net/
Что почитать?

• Lybniz 1.3.2 noarch для ScientificLinux 6
• Lybniz — строим графики математических функций

KSEG — свободная (GPL) программа которая даёт возможность создавать «живые чертежи» в планиметрии, в частности, для построений с помощью циркуля и линейки. KSEG также удобно использовать для построения качественных диаграмм.

Тип приложения: графические программы на основе библиотеки Qt
Сайт разработчика: http://www.mit.edu/~ibaran/kseg.html
Что почитать?

• KSEG. Материал из Википедии
• KSEG - программа для интерактивной геометрии

KmPlot — это графопостроитель алгебраических функций для KDE. Программа имеет мощный встроенный интерпретатор. Вы можете одновременно построить графики разных функций и комбинировать их для построения новых функций.

Тип приложения: графические программы на основе библиотеки Qt
Сайт разработчика: http://edu.kde.org/applications/all/kmplot/
Что почитать?

• Kmplot
• Man KmPlot
• KmPlot. Построить график функции.
• Справочное руководство KmPlot

JACAL - это интерактивная символьная математическая система, которая может оперировать и упрощать уравнения, скаляры, вектора и матрицы с простыми и многомерными значениями, алгебраические выражения,

Тип приложения: консольная программа
Сайт разработчика: http://people.csail.mit.edu/jaffer/JACAL.html

GraphThing - утилита для создания, изменения и изучения графов.

Тип приложения: другие программы для графического режима
Сайт разработчика: http://graph.seul.org/