Искусственный интеллект

[chelaut]

Нашел я этого ученого все таки. Не будем вдаваться в подробности, не это суть важно. ( это к тем с кем я общался)
Вопрос к знатокам!
Предположим, что некто, открыл новую аксиому в логике ( установил закономерности, которые происходят на невидимом для формального рассмотрения уровне рассуждения и доказательств и формализовал их), благодаря которой становиться возможным создание искусственного интеллекта. То есть если усовершенствовать язык программирования ПРОЛОГ, путем введения в него новых правил получим общий метод безошибочных рассуждений и доказательств.

Сам вопрос.

Предположем, что на основе открытия новой аксиомы становиться возможным создание программы выводящая самостоятельно теоремы из акиом. Какое практическое применение этой программе можно найти? И можно ли и нужно ли?

[Someone]

Мне кажется, надо попробовать такую программу сделать и посмотреть, что она будет выдавать. А там уже будет видно, какие у неё практические применения найдутся.

[chelaut]

Someone писал(а):

Мне кажется, надо попробовать такую программу сделать и посмотреть, что она будет выдавать. А там уже будет видно, какие у неё практические применения найдутся.

Ну тут вопрос в финансировании. Средств на самостоятельную разработку нет, а для того чтобы привлечь инвестора необходима практическая польза.

[Someone]

Под голословные заявления, конечно, деньги выпросить можно, но это как-то ...

[juna]

chelaut писал(а):

Предположим, что некто, открыл новую аксиому в логике ( установил закономерности, которые происходят на невидимом для формального рассмотрения уровне рассуждения и доказательств и формализовал их), благодаря которой становиться возможным создание искусственного интеллекта. То есть если усовершенствовать язык программирования ПРОЛОГ, путем введения в него новых правил получим общий метод безошибочных рассуждений и доказательств.

Этак можно до опровержения теоремы Гёделя о неполноте договориться.

chelaut писал(а):

Предположем, что на основе открытия новой аксиомы становиться возможным создание программы выводящая самостоятельно теоремы из акиом. Какое практическое применение этой программе можно найти? И можно ли и нужно ли?

Такие системы давно существуют и мало кому помогают доказывать настоящие теоремы.

[chelaut]

Someone писал(а):

Под голословные заявления, конечно, деньги выпросить можно, но это как-то ...

Да наврят ли можно.
Хотя если обладать соответствующим авторитетом то да.

Добавлено спустя 5 минут 1 секунду:

Re: Искусственный интеллект

]

Цитата:

Этак можно до опровержения теоремы Гёделя о неполноте договориться.

Ну можеи и можно.

Цитата:

Такие системы давно существуют и мало кому помогают доказывать настоящие теоремы.

А вот этого не знал. А не можете дать ссылку на более подробную информацию?
Вообще я имею ввиду то, что при введении новых правил в программу машина формирует новое понятие самостоятельно.[/quote]

[AlexDem]

chelaut писал(а):

Цитата:

Этак можно до опровержения теоремы Гёделя о неполноте договориться.

Ну может и можно.

Вряд ли... Если записать все $N$ формул, то возможных правил их преобразования будет $2^N$. Следовательно, $2^N - N$ из них мы ещё не записали. Не похоже, чтобы этот круг можно разорвать введением одной аксиомы.

[juna]

chelaut писал(а):

Вообще я имею ввиду то, что при введении новых правил в программу машина формирует новое понятие самостоятельно.

Вопрос в том, что такое понятие. Никакого понимания в настоящий момент машина осуществить не может. Правильнее говорить лишь об обработке информации. Какого типа грамматику задают правила вывода из аксиом, если тип 0 (по классификации Хомского), то вряд ли такой алгоритм будет иметь полиномиальную сложность, т.е. получать теоремы за приемлемое время. Если тип >0, то нельзя обработать даже естественный язык.

добавлено
Вот темы, где обсуждают аналогичные вопросы:
http://dxdy.ru/viewtopic.php?t=3647&start=0
http://dxdy.ru/viewtopic.php?t=2110&pos ... sc&start=0
http://www.cs.ru.nl/~freek/mizar/

[chelaut]

Цитата:

Вопрос в том, что такое понятие. Никакого понимания в настоящий момент машина осуществить не может. Правильнее говорить лишь об обработке информации. Какого типа грамматику задают правила вывода из аксиом, если тип 0 (по классификации Хомского), то вряд ли такой алгоритм будет иметь полиномиальную сложность, т.е. получать теоремы за приемлемое время. Если тип >0, то нельзя обработать даже естественный язык.

добавлено
Вот темы, где обсуждают аналогичные вопросы:
http://dxdy.ru/viewtopic.php?t=3647&start=0
http://dxdy.ru/viewtopic.php?t=2110&pos ... sc&start=0
http://www.cs.ru.nl/~freek/mizar/

Если в машине забито, что все лебеди белые, то при встрече с черным лебедем она ответит, что это не лебедь самостоятельно, безошибочно. Это и есть вывод нового понятия.
Понимания в настоящий момент она естественно совершить не может потому как необходимо применения новой логической аксиомы в силогизмах.

( Читаю ссылки, пока не нашел)[/quote]

[juna]

chelaut писал(а):

Если в машине забито, что все лебеди белые, то при встрече с черным лебедем она ответит, что это не лебедь самостоятельно, безошибочно. Это и есть вывод нового понятия.

На такое способна обычная силлогистика Аристотеля с шестью правильными модусами. И уж, конечно, это не введение нового понятия.
Посылки:
1. Все лебеди есть белые
2. Ни один белые не есть черные
3. Все нечто есть черные
Выводы:
1. Ни один черные не есть белые
2. Некоторые белые есть белые
3. Ни один черные не есть лебеди
4. Некоторые черные не есть лебеди
5. Ни один лебеди не есть черные
6. Некоторые лебеди есть белые
7. Некоторые лебеди не есть черные
8. Ни один нечто не есть белые
9. Ни один нечто не есть лебеди
10. Некоторые нечто не есть лебеди
11. Некоторые нечто не есть белые
12. Некоторые белые не есть черные
13. Ни один белые не есть нечто
14. Некоторые белые не есть нечто
15. Некоторые черные есть черные
16. Некоторые черные не есть белые
17. Ни один лебеди не есть нечто
18. Некоторые лебеди не есть нечто

[chelaut]

Артамонов Ю.Н. писал(а):

chelaut писал(а):

Если в машине забито, что все лебеди белые, то при встрече с черным лебедем она ответит, что это не лебедь самостоятельно, безошибочно. Это и есть вывод нового понятия.

На такое способна обычная силлогистика Аристотеля с шестью правильными модусами. И уж, конечно, это не введение нового понятия.
Посылки:
1. Все лебеди есть белые
2. Ни один белые не есть черные
3. Все нечто есть черные
Выводы:
1. Ни один черные не есть белые
2. Некоторые белые есть белые
3. Ни один черные не есть лебеди
4. Некоторые черные не есть лебеди
5. Ни один лебеди не есть черные
6. Некоторые лебеди есть белые
7. Некоторые лебеди не есть черные
8. Ни один нечто не есть белые
9. Ни один нечто не есть лебеди
10. Некоторые нечто не есть лебеди
11. Некоторые нечто не есть белые
12. Некоторые белые не есть черные
13. Ни один белые не есть нечто
14. Некоторые белые не есть нечто
15. Некоторые черные есть черные
16. Некоторые черные не есть белые
17. Ни один лебеди не есть нечто
18. Некоторые лебеди не есть нечто

Ну здесь обьяснение машине налицо и действительно понятия не возникает.
Я же говорю о совершенно другой форме.
ПОСЫЛКИ
Все птицы белые
Эта птица лебедь
Вывод
Все лебеди белые.
Забив эту логику в машину с аксиомой, ( повторюсь, без обьяснения) и встретив на своем пути черного лебедя она его и определит как черного самостоятельно.

Добавлено спустя 3 минуты 28 секунд:

И вообще посмотрите сколько выводов получилось, а здесь один единственный получается и притом верный!

[juna]

Здесь выводы все верные (если я программу правильно составил ).
Вот ваш пример.
Посылки
1. Все птицы есть белые
2. Все эта есть птицы
3. Все эта есть лебедь
4. Все лебедь есть эта
Выводы
1. Некоторые белые есть белые
2. Все эта есть белые
3. Некоторые птицы есть белые
4. Некоторые эта есть белые
5. Некоторые белые есть эта
6. Некоторые птицы есть птицы
7. Некоторые лебедь есть птицы
8. Некоторые лебедь есть белые
9. Все лебедь есть птицы
10. Все лебедь есть белые
11. Некоторые белые есть птицы
12. Некоторые птицы есть лебедь
13. Некоторые лебедь есть лебедь
14. Все лебедь есть лебедь
15. Некоторые эта есть эта
16. Некоторые эта есть птицы
17. Некоторые белые есть лебедь
18. Некоторые птицы есть эта
19. Некоторые лебедь есть эта
20. Некоторые эта есть лебедь
21. Все эта есть эта

Ваш вывод №10.
Если вы допускаете индуктивное утверждение, то заведомо поступаете некорректно, с точки зрения логики, а распространяя его на все возможные утверждения легко приходите к противоречиям. Ваш пример мне кажется неудачным.
О, если бы знать вашу волшебную аксиому!

[chelaut]

Артамонов Ю.Н. писал(а):

Здесь выводы все верные (если я программу правильно составил ).
Вот ваш пример.
Посылки
1. Все птицы есть белые
2. Все эта есть птицы
3. Все эта есть лебедь
4. Все лебедь есть эта
Выводы
1. Некоторые белые есть белые
2. Все эта есть белые
3. Некоторые птицы есть белые
4. Некоторые эта есть белые
5. Некоторые белые есть эта
6. Некоторые птицы есть птицы
7. Некоторые лебедь есть птицы
8. Некоторые лебедь есть белые
9. Все лебедь есть птицы
10. Все лебедь есть белые
11. Некоторые белые есть птицы
12. Некоторые птицы есть лебедь
13. Некоторые лебедь есть лебедь
14. Все лебедь есть лебедь
15. Некоторые эта есть эта
16. Некоторые эта есть птицы
17. Некоторые белые есть лебедь
18. Некоторые птицы есть эта
19. Некоторые лебедь есть эта
20. Некоторые эта есть лебедь
21. Все эта есть эта

Ваш вывод №10.
Если вы допускаете индуктивное утверждение, то заведомо поступаете некорректно, с точки зрения логики, а распространяя его на все возможные утверждения легко приходите к противоречиям. Ваш пример мне кажется неудачным.
О, если бы знать вашу волшебную аксиому!

Предположим я отправлю вам акиому. И предположим, что она оказывается истинной и недостающей.( ну в общем понятно) Можно ли гарантировать, что Вы не используете её в своих целях, забыв об этом ученом, который её открыл?

Вывод рассматривается в вопросе, что сделает машина когда встретит черного лебедя, а не в внутри данного силогизма. Она ответит, что это лебедь черный однозначно. Какой вывод сделает ваша машина?

[juna]

Я не понимаю, какой вывод делает ваш алгоритм.
Утверждаете, что все лебеди белые, а потом какую вы посылку добавляете? - Вот этот лебедь черный. Тогда вывод содержится в посылке. А если добавите, что ни один черный не есть белый, то, к тому же, легко приходите к противоречию.
Или вот это нечто есть черное. Вывод: это нечто - лебедь. Тогда это по меньшей мере неполная индукция, а она, как известно, нелогична.
Вообще, правильно утверждать, аккуратнее - некоторые лебеди есть белые, тогда остается место и для черных, розовых и т.д.

[chelaut]

Артамонов Ю.Н. писал(а):

Я не понимаю, какой вывод делает ваш алгоритм.
Утверждаете, что все лебеди белые, а потом какую вы посылку добавляете? - Вот этот лебедь черный. Тогда вывод содержится в посылке. А если добавите, что ни один черный не есть белый, то, к тому же, легко приходите к противоречию.
Или вот это нечто есть черное. Вывод: это нечто - лебедь. Тогда это по меньшей мере неполная индукция, а она, как известно, нелогична.
Вообще, правильно утверждать, аккуратнее - некоторые лебеди есть белые, тогда остается место и для черных, розовых и т.д.

Мы вносим алгоритм " Все лебеди белые!"
Вносим новое правило!
И при встрече черного лебедя не возникает ошибки!
Алгоритм перестраивается сам и выдаёт, что есть белый лебедь и есть черный лебедь!.
При этом мы не добавляем никаких посылок!
И именно исходная посылка не некоторые лебеди, а все!