Cтраница 3
При выполнении расчетов R следует принять равным расстоянию от центра залежи до водонефтяного контакта, а за рг принять давление на водонефтяном контакте. При кажущейся на первый взгляд сложности формул (3.26) и (3.29) их использование в сочетании с таблицами и графиками для вспомогательных функций Q ( т) не представляет труда. [31]
Исчисление G0 является частью исчисления G, предложенного Генценом. Исчисления генценовского типа по сравнению с изученными нами Исчислениями являются более удобными при анализе и поиске формальных доказательств. Это объясняется основной особенностью этих исчислений, которая, грубо говоря, состоит в том, что сложность формул при применении правил может только возрастать. Здесь мы лишь применим отмеченное выше свойство исчисления G0 для получения непротиворечивости ИВ, не прибегая к понятию интерпретации исчисления. В самом деле, рассмотрим секвенцию - Qo Индукцией по высоте легко заметить, что если D - доказательство секвенции S в исчислении GO и существует вхождение формулы в D, содержащее логическую связку Л или, то эта логическая связка обязана входить в S. Поэтому, если секвенция ( - Q0 доказуема в G0, то она может быть получена из аксиомы с помощью только правил 5) - 8), что очевидным образом невозможно. Применяя предложения 1 - 4, получаем непротиворечивость ИВ. [32]
Внимание исследователей привлекают и методы оценки сложности выводов. Сюда относятся такие проблемы, как отыскание сравнительно коротких формул, необходимо имеющих сложные доказательства, или формул, из которых уже сравнительно несложно можно получить большое количество результатов. Рассматриваются естественные меры сложности вывода: длина доказательства; время, требуемое для поиска вывода; сложность формул, фигурирующих в выводе, и др. В этой области методы теории доказательств смыкаются с методами теоретической кибернетики. [33]