Дискуссионный математический форумМатематический форум

Математический форум Math Help Planet

Обсуждение и решение задач по математике, физике, химии, экономике

Теоретический раздел
Часовой пояс: UTC + 3 часа [ Летнее время ]
MathHelpPlanet.com RSS-лента Математического форума

Часовой пояс: UTC + 3 часа [ Летнее время ]




Начать новую тему Ответить на тему  [ Сообщений: 2 ] 
Автор Сообщение
 Заголовок сообщения: Как составить алгоритм доказательства в ИВ?
СообщениеДобавлено: 07 апр 2015, 22:02 
Не в сети
Начинающий
Зарегистрирован:
22 фев 2014, 08:46
Сообщений: 7
Cпасибо сказано: 1
Спасибо получено:
0 раз в 0 сообщении
Очков репутации: 1

Добавить очки репутацииУменьшить очки репутации
Как составить алгоритм доказательства какого-нибудь общезначимого высказывания с помощью исчисления высказываний? Кто что думает?

Более подробно – ниже.

-

Как доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний? Например, x v !x? Можно использовать, к примеру, эту аксиоматику:
1: A -> ( B -> A)
2: (A -> B) -> (( A -> (B -> C)) -> (A -> C)
3: A & B -> A
4: A & B -> B
5: A -> (B -> A & B)
6: A -> A v B
7: B -> A v B
8: (A -> Q) -> ((B -> Q) -> (A v B ->Q))
9: (A -> B) -> ((A -> !B) -> !A)
10: !!A -> A

Я смотрю на примеры доказательств (static.php?p=formalizovannoye-ischisleniye-vyskazyvaniy - они не без помарок, но в общем понятные). Там вывод осуществляется из гипотез (которые неявно объединены в конъюнкцию), есть семантическое следование из них в доказываемое высказывание. Здесь же у нас нет гипотез, нет следования. Я где-то читал что-то в том роде, что мы можем вводить гипотезы - но как? Как конкретно доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний? Я пытаюсь решить (наметить план решения) третье задание следующего содержания (перепишу основную его часть):

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

Первое задание (тоже не очень понятно как решать) задаёт грамматику формами Бэкуса-Наура и его основная часть звучит следующим образом:

«Написать программу, проверяющую доказательства в исчислении высказываний на корректность. Входной файл представляет из себя последовательность высказываний, по высказыванию на строку. ... Результатом работы программы должен быть проаннотированный текст доказательства, касательно каждой строки должно быть указано, из чего и как она получается.»

Вернуться к началу
 Профиль  
Cпасибо сказано 
 Заголовок сообщения: Re: Как составить алгоритм доказательства в ИВ?
СообщениеДобавлено: 07 апр 2015, 23:05 
Не в сети
Light & Truth
Аватара пользователя
Зарегистрирован:
16 июл 2011, 08:33
Сообщений: 17738
Откуда: Беларусь, Минск
Cпасибо сказано: 1240
Спасибо получено:
3795 раз в 3514 сообщениях
Очков репутации: 713

Добавить очки репутацииУменьшить очки репутации
Chayepit, я читал Ваш вопрос "по диагонали". Поэтому моё сообщение может быть и невпопад. Но известно ли Вам это (автоматическое доказательство теорем): http://studopedia.net/10_57436_avtomati ... eorem.html. Прошу извинить, если что не так! :)

Вернуться к началу
 Профиль  
Cпасибо сказано 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 2 ] 

 Похожие темы   Автор   Ответы   Просмотры   Последнее сообщение 
Составить нормальный алгоритм Маркова

в форуме Дискретная математика, Теория множеств и Логика

deckvv

0

327

07 окт 2014, 21:29

Составить алгоритм определения и вычислить минимум функции

в форуме Исследование операций и Задачи оптимизации

Wild Heart

2

492

06 апр 2012, 09:37

Составить алгоритм решения задачи на языке паскаль

в форуме Информатика и Компьютерные науки

sasha20751

0

727

06 ноя 2012, 18:18

Задача в Турбо Паскаль - составить алгоритм и программу

в форуме Информатика и Компьютерные науки

Griffiss

0

464

07 май 2011, 09:42

Составить алгоритм нахождения в массиве выделяющихся чисел

в форуме Интересные задачи участников форума MHP

Christine

0

161

31 май 2015, 15:10

Доказательства

в форуме Алгебра

DeD

8

237

14 окт 2016, 10:46

Доказательства

в форуме Дискретная математика, Теория множеств и Логика

DeD

9

180

18 окт 2016, 11:10

Матрицы. Доказательства.

в форуме Линейная и Абстрактная алгебра

fimichsim

1

438

27 фев 2011, 17:51

Обоснование схемы доказательства

в форуме Дискретная математика, Теория множеств и Логика

Andy

1

96

09 янв 2017, 15:41

Проблема при разборе доказательства

в форуме Теория чисел

Free Dreamer

2

355

02 мар 2013, 01:06


Часовой пояс: UTC + 3 часа [ Летнее время ]



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 7


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Перейти:  

Яндекс.Метрика

Copyright © 2010-2018 MathHelpPlanet.com. All rights reserved