Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Формальная логика, отношение вывода которой не является монотонным.
Formal logic whose conclusion relation is not monotonic
Немонотонная логика – это формальная логика, отношение вывода которой не является монотонным. Иными словами, немонотонные логики разработаны для моделирования и представления отменяемых выводов, то есть такого типа умозаключений, в которых рассуждающие приходят к предварительным заключениям, позволяя им отказаться от этих заключений на основании новых данных. Большинство изучаемых формальных логик обладают монотонным отношением следования, что означает, что добавление формулы к исходным данным никогда не приводит к сокращению множества выводимых заключений. Интуитивно, монотонность указывает на то, что получение новых знаний не может уменьшить объем уже известных фактов. Монотонные логики не способны решать различные задачи рассуждения, такие как рассуждение по умолчанию (выводы делаются только из-за отсутствия доказательств обратного), абдуктивное рассуждение (выводы выводятся как наиболее вероятные объяснения), некоторые важные подходы к рассуждению о знаниях (незнание вывода должно быть отменено, когда вывод становится известным) и, аналогично, пересмотр убеждений (новые знания могут противоречить старым убеждениям).
A non monotonic logic is a formal logic whose conclusion relation is not monotonic. In other words, non monotonic logics are devised to capture and represent defeasible inferences, i. e., a kind of inference in which reasoners draw tentative conclusions, enabling reasoners to retract their conclusion(s) based on further evidence. Most studied formal logics have a monotonic entailment relation, meaning that adding a formula to the hypotheses never produces a pruning of its set of conclusions. Intuitively, monotonicity indicates that learning a new piece of knowledge cannot reduce the set of what is known. Monotonic logics cannot handle various reasoning tasks such as reasoning by default (conclusions may be derived only because of lack of evidence of the contrary), abductive reasoning (conclusions are only deduced as most likely explanations), some important approaches to reasoning about knowledge (the ignorance of a conclusion must be retracted when the conclusion becomes known), and similarly, belief revision (new knowledge may contradict old beliefs).
Абдуктивные рассуждения
Абдуктивное рассуждение — это процесс вывода достаточного объяснения известных фактов. Абдуктивная логика не должна быть монотонной, поскольку вероятные объяснения не обязательно являются правильными. Например, вероятным объяснением мокрой травы является дождь; однако это объяснение необходимо отозвать, узнав, что настоящей причиной мокрой травы был поливочный дождеватель. Поскольку старое объяснение (дождь) отзывается из-за добавления новой информации (работал дождеватель), любая логика, моделирующая объяснения, является немонотонной.
Abductive reasoning is the process of deriving a sufficient explanation of the known facts. An abductive logic should not be monotonic because the likely explanations are not necessarily correct. For example, the likely explanation for seeing wet grass is that it rained; however, this explanation has to be retracted when learning that the real cause of the grass being wet was a sprinkler. Since the old explanation (it rained) is retracted because of the addition of a piece of knowledge (a sprinkler was active), any logic that models explanations is non monotonic.
Разумные рассуждения о знании
Если логика включает формулы, означающие, что что-то неизвестно, то эта логика не должна быть монотонной. Ведь получение информации, которая ранее была неизвестна, приводит к удалению формулы, констатирующей незнание этого факта. Это второе изменение (удаление, вызванное добавлением) нарушает условие монотонности. Автоэпистемическая логика является логикой рассуждений о знании.
If a logic includes formulae that mean that something is not known, this logic should not be monotonic. Indeed, learning something that was previously not known leads to the removal of the formula specifying that this piece of knowledge is not known. This second change (a removal caused by an addition) violates the condition of monotonicity. A logic for reasoning about knowledge is the autoepistemic logic.
Пересмотр убеждений
Ревизия убеждений — это процесс изменения системы убеждений для согласования с новым убеждением, которое может быть несовместимо с существующими. При условии, что новое убеждение считается истинным, некоторые из прежних убеждений должны быть отозваны для поддержания непротиворечивости. Этот отказ от прежних убеждений в ответ на добавление нового делает любую логику ревизии убеждений немонотонной. Подход ревизии убеждений является альтернативой параконсистентным логикам, которые допускают противоречия, а не стремятся к их устранению.
Belief revision is the process of changing beliefs to accommodate a new belief that might be inconsistent with the old ones. In the assumption that the new belief is correct, some of the old ones have to be retracted in order to maintain consistency. This retraction in response to an addition of a new belief makes any logic for belief revision non monotonic. The belief revision approach is alternative to paraconsistent logics, which tolerate inconsistency rather than attempting to remove it.
Теоретические доказательства против теоретических моделей формализации немонотонных логик
Теоретическая формализация доказательств немонотонной логики начинается с принятия определенных немонотонных правил вывода, а затем определяет контексты, в которых эти немонотонные правила могут применяться в допустимых выводах. Обычно это достигается посредством уравнений с фиксированной точкой, связывающих множества посылок и множества их немонотонных заключений. Логика по умолчанию и автоэпистемическая логика – наиболее распространенные примеры немонотонных логик, формализованных таким образом. Модельно-теоретическая формализация немонотонной логики начинается с ограничения семантики подходящей монотонной логики до определенных специальных моделей, например, минимальных моделей, а затем выводит набор немонотонных правил вывода, возможно, с ограничениями на контексты их применения, так чтобы полученная дедуктивная система была корректной и полной относительно ограниченной семантики. В отличие от некоторых теоретико-доказательных формализаций, страдавших от известных парадоксов и часто трудно поддававшихся оценке с точки зрения соответствия интуитивным представлениям, которые они должны были отражать, модельно-теоретические формализации были свободны от парадоксов и практически не оставляли места для путаницы относительно охватываемых ими немонотонных схем рассуждений. Примеры теоретико-доказательных формализаций немонотонного рассуждения, обнаруживших нежелательные или парадоксальные свойства, либо не отразивших желаемые интуитивные представления, которые были успешно (в соответствии с соответствующими интуитивными представлениями и без парадоксальных свойств) формализованы модельно-теоретическими средствами, включают в себя циркумскрипцию первого порядка, предположение о замкнутом мире и автоэпистемическую логику.
Proof theoretic formalization of a non monotonic logic begins with adoption of certain non monotonic rules of inference, and then prescribes contexts in which these non monotonic rules may be applied in admissible deductions. This typically is accomplished by means of fixed point equations that relate the sets of premises and the sets of their non monotonic conclusions. Default logic and autoepistemic logic are the most common examples of non monotonic logics that have been formalized that way. Model theoretic formalization of a non monotonic logic begins with restriction of the semantics of a suitable monotonic logic to some special models, for instance, to minimal models, and then derives a set of non monotonic rules of inference, possibly with some restrictions on which contexts these rules may be applied in, so that the resulting deductive system is sound and complete with respect to the restricted semantics. Unlike some proof theoretic formalizations that suffered from well known paradoxes and were often hard to evaluate with respect of their consistency with the intuitions they were supposed to capture, model theoretic formalizations were paradox free and left little, if any, room for confusion about what non monotonic patterns of reasoning they covered. Examples of proof theoretic formalizations of non monotonic reasoning, which revealed some undesirable or paradoxical properties or did not capture the desired intuitive comprehensions, that have been successfully (consistent with respective intuitive comprehensions and with no paradoxical properties, that is) formalized by model theoretic means include first order circumscription, closed world assumption, and autoepistemic logic.