Разработка формальной системы

| Категория реферата: Рефераты по математике
| Теги реферата: реферат на тему україна, база рефератов
| Добавил(а) на сайт: Angelika.

Синтаксис термов:
Терм - всякая предметная константа, предметная переменная либо функциональная форма.
Предикатная форма – предикатная константа, соединяющаяся с подходящим числом терм:

P(t1, .., tm);

P( ).
Если fn – функциональный символ, t1, t2, …, tn – термы, то fn (t1, t2, …, tn) также терм.
Понятие формулы в логике определим следующим образом:

. всякая предикатная форма есть формула;

. если А – формула, то А-1 тоже формула;

. если А и В - формулы, то А + В, А * В также формулы;

. если А - формула и хА - переменная, то (xА и (xA - формулы;

. других формул нет.
Для данной формальной логической системы справедливы следующие аксиомы:

1. E (f+(A, 0), A),

2. E ( f+(A, A), A),

3. ((i | i=[pic]) E (f*(Ai, f-1(Ai)),1i),

4. E (f+(A, B), f+(B, A)),

5. ((A | f-1(Ai) = 1i , i=[pic]) E (f*(Ai, 1i),Ai)
Формула общезначима (является тавтологией), если она истинна в любой интерпретации.
Формула невыполнима (противоречива, тождественно ложна), если она при всех интерпретациях является ложной.
Множество теорем определим как множество общезначимых формул.
Приведем примеры логического вывода:
1)Пусть А, В, С- любые формулы, тогда выводами являются следующие последовательности: а)A ( (B ( A); б)A ( (B ( A), A ( (B ( A); в)A ( (A ( A), (A ( (B ( C)) ( ((A ( B) ( (A ( C)) г)((A ((B) ( (B ( A), B ( (A ( B),(A ( ((B ( (A); д)(A ( (A ( A)) ( ((A ( A) ( (A ( A)), (A ( (A ( A)),(A ( A) ( (A ( A):
[pic].
2)Выведем: ? A(u) ( (uA(u), где A(u) – любая предикатная формула.
Формула(u(A(u) ( (A(u), согласно аксиоме (xF(x) ( F(y), выводима. Формула
(p ( (q) ( (q ( (p) – тавтология и следовательно выводима. Из этого следует, что предикатная формула (A ( (B) ( (B ( (A), где А, В- любые формулы, выводима в исчислении предикатов. Тогда выводима и формула [pic].
Отсюда по правилу заключения ?A(u)(((u(A(u), то есть ?A(u) ( (uA(u).
Также можно использовать и следующие правила вывода:
? A ( B, ? B ( C, то ? A ( C
A? B, C ? D, B, D ? E, то A, B ? E
? A ( (B ( C), то? B ( (A ( C)
? A( (B ( C), то A + B ( C
? A + B ( C, то? A ( (B ( C)
? - символ « выводимости »

10. Блок-схема программы, демонстрирующей отношение и основные операции алгебраической системы. Пример выполнения программы.
Ниже приведена блок-схема программы, содержащая функции и процедуры, которые реализуют основные операции и отношения алгебраической системы, и пример работы программы, в которой пользователем задаются 2 пазла – А и В и вычисляется С = A + B, D = A * C, происходит сравнение А и В.

[pic]

--------------------
[1] Все доказательства приведены для отношения больше(меньше) по количеству вогнутостей; для отношения больше(меньше) по количеству выпуклостей доказательство аналогичное.
[2] Для равенства по количеству вогнутостей и выпуклостей применяется аналогичное доказательство.

--------------------
[pic]

[pic]

[pic]

[pic]