x = o, (26); T8 |- x + a = a x = o, (3); и другие. Здесь, например, T2. |- a + b = b + a , (4) обозначает теорему номер два (закон коммутативности), доказательство которой на ЭВМ автоматически нумеруется 10-ю формулами, из которых только 4 непосредственно задают её вывод в то время как 6- ю формулами нумеруются аксиомы, знак доказуемости |- и формула, которую нужно доказать. Если в качестве групповой операции выбрано умножение, то наличие приведенных выше формализованных доказательств позволяет без труда получить теоремы: T1´. |- (ab)c = a(bc), T2´. |- ab = ba, T3´. |- a 1 = a, T4´. |- a a - 1 = 1, T5´. |- a -1 a = 1, T6´.|- 1 a = a, T7´. |- a x = ax = 1, T8´. |- x a = a x = 1 и другие. Если вместо T4´ (T5´ соответственно) взять в качестве аксиом a ≠ o a a -1 = 1 и добавить закон дистрибутивности a (b +c) = ab + ac, то получим поле с выделенными в нём теоремами теории групп, а если ещё добавить аксиомы дифференцирования [2] D(a+b) = Da + Db, Dab = a Db + b Da, то получим теорию DF дифференциальных полей, основной изучаемой моделью которой является поле мероморфных функций комплексного переменного. Когда к теории добавляется уравнение Абеля, определяющее алгебраические функции, а также уравнение [2] Dx = Dy/y, задающее логарифм и экспоненту, то это позволяет ввести элементарные функции, а классификация Лиувилля этих функций позволит построить счетное множество дифференциальных алгебр, простейшей из которых будет ({ sh x , ch x }, D). К алгебрам присоединяется и изучается операция интегрирования [2].
СПИСОК ЛИТЕРАТУРЫ:
- Смирнов В.А., Маркин В.И., Новодворский А.Е., Смирнов А.В.Логика и компьютер, Вып. 3. Доказательство и его поиск. - М.: Наука, 1996. - 255 c.
- Дэвенпорт Дж. Интегрирование алгебраических функций. - М.: Мир, 1985. - 190 c.