Обычно технология планирования методом построения доказательства имеет следующий вид. Сначала делается попытка найти вывод целевого описания из исходного. Если такой вывод найден, то план построен. Если это сделать не удается, что определяется на основе некоторого принципа остановки, подобного тому, который мы указали для программы ЛОГИК-ТЕОРЕТИК, то к исходному описанию применяется некоторое эвристическое правило вывода, и процесс доказательства повторяется уже при новом исходном описании. Методы такого типа сейчас являются основными при построении планировщиков в самых различных областях. [c.226]
Независимо от метода построения выборки она должна предоставлять аудитору надежную возможность сбора аудиторских доказательств. [c.152]
Выбор наиболее целесообразного сочетания методов проведения исследовательских работ дополняется на стадии НИР подбором соответствующих средств исследования, под которыми понимается совокупность материальных и нематериальных элементов, используемых для изучения объектов в процессе проведения исследования и обобщения научных данных. К материальным средствам исследования относятся приборы, экспериментальные установки и стенды, ЭВМ и т. п., к нематериальным — методы вычислений, программы для ЭВМ, математические теории, логические правила построения определений, выводов, доказательств. [c.50]
В соответствии с теоремой 4.12 проверка справедливости соотношения у >м У" сводится к решению канонической задачи линейного программирования (4.27). Это решение может быть осуществлено с помощью известного алгоритма симплекс-метода. Такой способ проверки соотношения у1 >м у" удобен при создании общего алгоритма построения оценки сверху в случае конечного множества возможных векторов Y. Если же требуется решить задачу невысокой размерности вручную , то более удобным оказывается использование следующего результата, который представляет собой частный случай теоремы 4.12, установленный в ходе доказательства этой теоремы. [c.127]
Аналитический подход в первую очередь затрагивает тестирование и обоснование программ после того, как они написаны, чтобы повысить их надежность. Он включает традиционные методы отладки программ, средства доказательства правильности программ, различные средства автоматического тестирования. Конструктивный подход использует набор надежных программных средств для разработки надежного ПО, которые принято называть структурным программированием. Этот подход включает построение средств, использующих просмотр сверху вниз и формальные спецификации, и средства кодирования с применением простых управляющих структур. [c.260]
Целью настоящего раздела было естественное расширение построенной ранее схемы, чтобы она охватывала более общий случай, когда планы формируются моделью, но выполняются в реальном мире. В подтверждение можно привести практические трудности, с которыми сталкиваются в настоящее время подходы, основывающиеся на доказательстве теорем методом резолюции (см. [33]). Проверка новых формулировок и программ на конкретных конструкциях робота является задачей ближайшего будущего. [c.403]
Разумеется, важно разработать некоторые средства для построения планов с циклами или другие методы равной силы. Я не вижу каких-либо существенных проблем, которые могли бы возникнуть при формулировании системы в терминах теории алгоритмов, и, по-видимому, ограничения, которые накладывают аксиомы причинности на формирование плана, являются всего лишь результатом сравнительно слабого еще развития теории. Например, вызывает большие трудности доказательство желаемых свойств программ, таких, как эквивалентность и конечность, в то время как относительная польза от этого невелика. Так, в случае простых циклов индуктивное предположение при доказательстве конечности должно гарантировать, что на предварительные условия свободы п-й итерации не могло повлиять выполнение (п— 1)-й итерации. [c.469]
На рис, 7.3 в двойных логарифмических координатах представлена кривая зависимости R/S от N для Н = 0.5, построенная по данным из рис. 7.1. Эти данные были получены с помощью генератора псевдослучайных чисел с гауссовскиМ выходом и показывают Н = 0.55 0.1. Эта оценка немного выше, чем ожидалось, но эти псевдослучайные числа сгенерированы детерминистическим алгоритмом. Это может быть причиной смещения. Важно заметить, что Д/5-анализ — это исключительно устойчивый метод. В его основе нет предположения о гауссовском распределении. Найденное значение Н = 0.50 не является доказательством того, что налицо [c.96]
Доказательство теоремы проводится методом математической индукции. Для р = 2 оно верно. Предположим, что оно верно для всех р р, и докажем, что оно верно и для р + 1. Не нарушая общности, можно считать, что перестановка а соответствует естественной нумерации координат. Обозначим Gp и Тр граф структуры зависимостей X и произвольное дерево, построенные на V (Gp) = (0, 1, 2,. .., р . Тогда Е (GJ)+1)= = (Gp) + (р + 1, / (р + 1)) и Е (Тр+1) = Е(ТР + (р +1, Л), где k < р + 1 — некоторая вершина G. Если k = / (р + 1), то утверждение теоремы верно согласно предположению, так как [c.153]
Правильность данных о наличии технических средств проверяется балансовым методом наличие на данный момент (предположим на 1 января 1955 г.) выводится из наличия на предыдущий отчётный момент (т. е. из наличия на 1 января 1954 г.), суммирования поступлений (предположим по локомотивам — вновь построенных, принятых от других министерств) и вычитания всех снятых с учёта за год (исключённых из инвентаря, переданных установленным порядком другим министерствам). Совпадение данных о наличии по балансу и по непосредственному подсчёту является доказательством достоверности этих данных. [c.534]
Данный стандарт применяется как к выборкам, построенным статистическим методом (случайная выборка), так и ко всем другим выборкам. Вне зависимости от того, каким методом построена выборка, она должна представлять надежную возможность для сбора аудиторских доказательств. [c.30]
Подобное доказательство может строиться на том, что колеблемость доходов с бизнеса (измеренная, к примеру, показателем 8 ) сопровождается тем, что коэффициент р по профильной для бизнеса отрасли в стране или в мире невысок (незначительно больше единицы или даже меньше единицы). Тогда объяснить колеблемость доходов с бизнеса можно действительно только преобладающим влиянием на нее несистематических рисков. Если же складывается обратная ситуация, то применение метода кумулятивного построения ставки дисконта некорректно (если не сказать недобросовестно) и следует использовать модель оценки капитальных активов или иные подхода. [c.44]
Целью данного стандарта является установление норм и правил построения аудиторской выборки, а также оценки результатов выборочной проверки. Настоящий стандарт в равной степени относится как к статистическому, так и к нестатистическому методам выборочной проверки, поскольку любой из указанных методов, при уместном применении, способен обеспечить достаточное аудиторское доказательство. [c.120]
Именно на этом пути явного построения мартингальной меры и будет далее строиться доказательство, следуя идеям работы Роджерса (L. С. G. Rogers) [407] и методам построения эквивалентных мер, основанным на "условных преобразованиях Эшера" [c.46]
Модификации системы STRIPS, система ABSTRIPS, а также дедуктивные вопросно-ответные системы QA-3 и QA-4, идеи которых легли в основу многих планирующих систем, описаны в монографии [5.4]. Пионерской работой в области метода резолюции была работа [5.5]. Различные способы повышения эффективности стратегий, используемых при нахождении резольвент, описаны в монографии [5.6]. Поиск таких улучшений все время продолжается, так как метод резолюции остается одним из самых популярных среди разработчиков многих практических систем. Однако он не единственно возможный или самый эффективный. Например, обратный метод поиска доказательства, предложенный в свое время известным советским логиком С. Ю. Маеловым [5.7], во многих отношениях превосходит метод резолюции. Этот метод реализован, например, в системе планирования СФИНКС, описанной в уже упоминавшейся монографии [5.4]. Трудности, характерные для имеющихся сейчас процедур вывода, и возможность совмещения этих процедур с некоторыми эвристическими приемами обсуждалась многими авторами. Сводка соответствующего материала приведена в [5.8] и [5.9]. В монографии [5.4] проводится сравнение чисто логических стратегий планирования с теми стратегиями, которые мы обсуждали в 5.7. Некоторые дополнительные соображения по поводу методов планирования, опирающихся на вывод в исчислении предикатов, можно найти в работе [1.1]. Рассуждения о необходимости нелинейных планов, приведенные в конце 5.2, заимствованы из работы [5.10], где излагается описание планирующих систем, допускающих построение немонотонных планов. [c.268]
Изучаемые признаки, например Y и X, имеют линейную тенденцию. При этом уравнения множественной регрессии себестоимости добычи нефти и газа, построенные методами коррелирования отклонений от уровней динамических рядов и коррелирования уровней динамических рядов, включая фактор времени, тождественны, так как между отклонениями [Yx — Y(t) и [X — X(t-,] существует функциональная связь. Для доказательства этого используем исходные данные об уровнях себестоимости добычи нефти и газа по Укрнефти и дебите на скважино-месяц отработанный за период 1956—1971 гг. (табл. 21). [c.76]
Представляется, что действительный прогресс может быть достигнут только построением более жесткой управляющей структуры, внутри которой проводится поиск доказательства. Примером является разновидность супервизора, в общих чертах обрисованного Маккарти [7]. Аксиомы, связанные с таким специфическим понятием, как понятие причинности, как нам кажется, должны потребовать специфического обращения. Не следует ожидать, что будет найден общий метод, подобный эвристическому поиску, который подходил бы для любой системы аксиом и позволил бы адекватно учитывать всю их совокупность. [c.471]
Человек, обладающий интеллектом, глубоко продумывает свой прошлый опыт и извлекает из него уроки. Современные же системы для доказательства теорем и решения задач, постоянно углубляя свои способности к мышлению, полностью пренебрегают предыдущим опытом. Решатель задач, построенный для любого из современных методов организации решающих систем (таких, как метод резолюций [1], GPS [2], REF-ARF [3]), решает ту же задачу каждый раз одним и тем же способом. Такие системы не в состоянии использовать сходство между новыми и старыми задачами для ускорения поиска решения новых задач. Система ZORBA, описанная в этой статье, является примером системы, работающей с некоторым типом аналогий3). Это первый пример системы, которая способна обнаружить отношение аналогии между двумя задачами и выдает на выходе такую информацию, которая может быть полезна для программы решателя задач с точки зрения сокращения времени поиска решения. [c.473]
Если же построения плана рассматривать просто как метод доказательства необходимости и целесообразности перехода к травополью, то совершенно ясно, что, во-первых, для этого были не нужны столь обширные и головоломные исчисления об организации хозяйства и его балансе, во-вторых, эти исчисления сами по себе не убеждают в необходимости и возможности повсеместного перехода Сибирского края к травопольной системе. Путь обоснования этого лежвл бы в плоскости более глубокого анализа фактической эволюции сельского хозяйства Сибири, в анализе общих перспектив рынка, промышленности по переработке, путей сообщения и т.д. Но именно этого в достаточной степени не дано в работе Сибкрайземуправления и именно эти соображения привели, например, Земплан НКЗ РСФСР к выводу, что намеченная планом задача всеобщего перехода сибирского сельского хозяйства к травополью нереальна. [c.589]
Большинство рекламных обращений являются комбинацией двух основных литературных техник лекции и драмы. ЛЕКЦИЯ — это серьезная, структурированная информация, изложенная устно. ДРАМА — это история или пьеса, построенная вокруг героев в какой-то ситуации. Обе техники используются в рекламе. Лекции являются формой прямого обращения. С точки зрения стилистики говорящий обращается к аудитории по телевидению или с печатных страниц. Аудитория принимает обращение на расстоянии . Говорящий представляет доказательства (в широком смысле этого слова) и использует метод аргументированного убеждения аудитории. Некоторые лекции основаны на мнении таких авторитетных лиц или экспертов в определенных технических областях, как Майкл Джордан для Nike и Чак Егер (бывший испытатель) для автомобильных запасных частей Del o. [c.427]