Формальный вывод - Большая Энциклопедия Нефти и Газа, статья, страница 3
Молоко вдвойне смешней, если после огурцов. Законы Мерфи (еще...)

Формальный вывод

Cтраница 3


Чтобы в дальнейшем всюду было ясно, почему мы интересуемся формальными системами, которые мы рассматриваем, и каким образом они представляют собой формализации тех разделов логики и математики, с которыми содержательно мы уже знакомы, мы в этой книге будем указывать возможные интерпретации и пользоваться естественной терминологией, например, выражением доказательство для формальных выводов и и как названием символа &. Это необходимо для полного достижения нашей цели, хотя интерпретация сама по себе чужда метаматематике.  [31]

Поскольку cPv d ( Rev) i ( Imi), данное представление все еще задается двойным интегралом, но оно содержит только проекционные операторы и существенно проще представления (11.6.10) через четырехкратный интеграл. Формальный вывод (11.8.1) будет сделан ниже, в разд.  [32]

Их можно, конечно, получить эвристическим методом, так как функция D ( r p, TO) пропорциональна вероятности выхода фотона из среды. Однако здесь мы предпочли формальный вывод, чтобы показать, как он производится.  [33]

Разработка будет неформальной; формальный вывод CFR появится в разд.  [34]

Все члены в правой части уравнения (8.32) можно ( в принципе) вычислить для данной произвольной функции распределения электронов и ионов. В работе [359] имеется формальный вывод уравнения (8.32) на основе теории Боголюбова - Борна - Грина - Кирквуда - Ивона.  [35]

Спеннер и Геббард [27] отмечают, что метод разбиения представляет собой частный случай выборки по значимости, причем более простой для использования, так как отпадает необходимость в подборе неадекватного распределения. Эти авторы приводят, кроме того, формальный вывод оценок по методу русской рулетки и дают оценки эффективности метода разбиения.  [36]

Метод определения коэффициента активности по изменению упругости паров растворителя над раствором солей различной концентрации в конечном итоге также учитывает свободную энергию разведения. Поэтому если не связывать результаты подсчетов с формальными выводами о сверхидеальных свойствах растворов, то расчеты коэффициентов активности не приводят к ошибочным результатам.  [37]

Для этого надо просто повторить обычные рассуждения, употребляемые для этой цели в арифметике. Однако следует заметить, что такие доказательства являются не формальными выводами в самой ограниченной арифметике, а содержательными рассуждениями об ограниченной арифметике.  [38]

L, Percus J. K., Statistical then-mpdynamics of non-uniform fluids, дается формальный вывод уравнения Орнштейна - Цернике ( 58), которое они считают точным. Однако в настоящее время еще не ясно, приводит ли это к такому методу последовательных приближений, при котором можно было бы исходить из уравнения ( 69) в качестве первого приближения.  [39]

Подробнее об этом говорится в следующей главе. Главная выгода, получаемая от неформальных доказательств, возникающих из развития формальных выводов, заключается в том, что создается система, в рамках которой можно объективно, механическим путем решить, в случае разногласий, представляет ли собой спорное доказательство действительно доказательство.  [40]

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

Соединение эвристических методов и приемов с мыслительным моделированием ведет к сочетанию свободных суждений, включая правдоподобные суждения, с гипотетико-дедуктивными способами суждений. В ходе поиска на основе мысленных моделей решение поставленных задач происходит с использованием известных формальных выводов и знаний предмета, а также предположений, догадок и данных опыта. Таким образом, мыслительное моделирование как эвристический прием позволяет устанавливать пути достижения целей по определенной модели ( программе), где не все компоненты и данные логически определены.  [42]

Разные логические теории имеют свои преимущества при реализации моделей в разных микромирах. Так, например, семантика силлогистики Аристотеля очень близка к естественному языку, поэтому результаты формального вывода легко интерпретировать. Выводы, получаемые на основе исчисления предикатов, уже не в полной мере совпадают с семантикой естественного языка, их труднее интерпретировать, однако модели на основе исчисления предикатов получаются гораздо более компактными и, как следствие, обозримыми. Заде позволяют оперировать размытыми понятиями, однако такие результаты и интерпретировать труднее и даже не всегда возможно.  [43]

Теоремы в &, &, 0 называются доказуемыми формулами или, точнее, формулами, доказуемыми в У. По определению формула а является доказуемой в У в том и только в том случае, когда существует формальное доказательство формулы а в 9, т.е. формальный вывод формулы а в S из пустого множества формул.  [44]

Автоматическое доказательство теорем ведет свое начало от основополагающих работ Эрбрана, который еще в 30 - х годах XX в. В 60 - е годы усилиями Ньюэлла и Саймона был создан общий решатель проблем, доказывающий теоремы формальной логики, разработанной Расселом и Уайтхедом, которые считали, что для математики достаточно иметь формальный вывод теорем из основных аксиом.  [45]



Страницы:      1    2    3    4