(←) предыдущая запись ; следующая запись (→)
А дальше есть разные варианты усложнить модель так, чтобы машина делала больше, а человек меньше.
Например, мы можем строить системы, основанные на математической логике.
Разберёмся! Логика — это наука про то, как по формальным правилам переписывать одни тексты в другие.
Пусть у нас есть текст из четырёх предложений: «Сократ — человек. Человек — млекопитающее. Человек смертен. Млекопитающие — позвоночные животные».
Скомбинировав посылки текста (они называются аксиомами), мы можем сделать новое утверждение: «Сократ смертен».
Это предложение можно, например, дописать в конец нашего текста. И дальше использовать в качестве посылки в каких-то новых умозаключениях.
Отметим, что нам вообще неважно, что означает слово «смертен», кто такой Сократ и что за зверушка такая «человек». Мы чисто формально воспользовались правилом: из двух утверждений
«X является объектом типа Y» и «объекты типа Y имеют свойство Z» следует справедливость утверждения «X имеет свойство Z».
Вообще говоря, из наших посылок мы могли бы вывести и другое утверждение: «Сократ — млекопитающее». С точки зрения формальной логики это настолько же разумное утверждение, как то, что он смертен.
Теперь представьте, что мы хотим доказать, что Сократ — позвоночное животное (например, чтобы применить к нему правила касательно юридического статуса позвоночных животных; вы ведь ещё не забыли, что мы про юриспруденцию?). Значит нам нужно шаг за шагом применять наше правило преобразования — пока единственное — к посылкам, пока мы не получим нужное следствие. Цепочка таких преобразований называется логическим выводом.
Казалось бы, всё просто. Но проблема в том, что на каждом шаге мы можем комбинировать правила различными способами. Некоторые преобразования приближают нас к цели, другие — не приближают. Некоторые утверждения вообще невозможно доказать.
Например, утверждение «Сократ не является млекопитающим» недоказуемо. В некоторых логических системах мы могли бы его опровергнуть (для этого понадобилось бы ввести ещё несколько правил преобразований утверждений), но в нашей упрощённой системе нет правила исключённого третьего, поэтому мы не можем показать, что такое утверждение противоречило бы нашим знаниям.
А самые чудовищные утверждения нельзя ни доказать, ни опровергнуть. Причём это совершенно рядовая ситуация. Скажем, исходя из наших четырёх аксиом, мы ничего не сможем сказать про справедливость утверждения «Цой смертен», потому что не знаем, человек ли он или.
Получается, мы теоретически можем доказывать или опровергать некоторые утверждения. Но на практике это может занять непредсказуемо много времени (вплоть до бесконечного). Компьютер, как и человек, будет перебирать последовательности силлогизмов, пока не добьётся успеха или не отчается.
В целом выглядит так, что логика — разумный сеттинг для работы с юридическими текстами. Беда только в том, что в сколько-нибудь сложных логических системах нет гарантий того, что эти цепочки рассуждений когда-либо завершатся. Да и как работать с неизбежными противоречиями, неясно.
(2/n)