Cтраница 2
Приведенный конкретный пример в достаточной степени разъясняет смысл разделения механики на механику точки, твердого тела и упругих тел. В природе не существует ни материальных точек, ни твердых ( недеформируемых) тел, ни абсолютно упругих тел. Все это абстракции, которыми приходится пользоваться в науке для того, чтобы правильно отразить те свойства реальных объектов, которые необходимо учесть при решении поставленной задачи. Применяемые абстракции никогда не отражают полностью всех свойств реального объекта. Но это и не обязательно, если те свойства реального объекта, которые применяемая абстракция не отражает, не сказываются сколько-нибудь заметно на характере изучаемого движения; между тем применение абстракций существенно упрощает решение всякой задачи. Если бы мы пытались всякий раз полностью учесть все свойства реального тела, движение которого должно быть рассмотрено, то задача настолько усложнилась бы, что решить ее практически было бы невозможно. Поэтому всегда следует стремиться применять абстракции, правильно отражающие только те свойства реальных объектов, которые играют определяющую роль в рассматриваемом движении. [16]
Определяется класс функций, называемых абстракциями, и приводятся их примеры. Для того чтобы найти доказательство дизъюнкта С из S, достаточно найти доказательство из Г и попытаться обратить функцию абстракции. Предлагается несколько стратегий доказательства теорем, основанных на этой идее. Приводится также метод употребления нескольких абстракций одновременно, что требует использования мультидизъюнк-тов, которые являются мультимножествами литер, и связанных с ними функций m - абстракции. Некоторые абстракции особенно интересны, поскольку они соответствуют отдельным интерпретациям множества дизъюнктов S. Применение абстракций дает возможность реализовать преимущества стратегий поддержки в произвольных полных резолюционных стратегиях. [17]
Такая стратегия универсальна и. Каждый шаг поиска в ней осмыслен и нетривиальным образом управляется структурой задачи в целом, а не только такой локальной информацией, как способность двух дизъюнктов резольвировать согласно определенной стратегии. Мы считаем такое локальное поведение одним из самых слабых мест современных систем доказательства теорем. Использование аналогии имеет дополнительное преимущество в том, что стратегия поиска становится все более и более ограничивающей по мере увеличения глубины вывода. При завершении поиска число возможных выборов более ограничено, чем в середине, несмотря на то что стратегия основана на прямых рассуждениях. Это резко отличается от ситуации, характерной для традиционных стратегий, в которых поисковое пространство с ростом глубины, по-видимому, экспоненциально увеличивается в объеме. Применение абстракции допускает также возможность нескольких уровней абстракции, причем каждый последующий уровень содержит меньше информации, чем предыдущий. Поиск на каждом уровне может управляться поиском на следующем, более высоком уровне абстракции. [18]