Логика в информатике: основные направления и приложения

Введение

Академическая конференция LICS. Академическая дисциплина. "Логика в информатике" охватывает область пересечения логики и информатики. Данную тему можно разделить на три основных направления: теоретические основы и анализ; использование компьютерных технологий для помощи логикам; применение концепций логики в компьютерных приложениях.

Теоретические основы и анализ

Логика играет фундаментальную роль в информатике. Некоторые из ключевых областей логики, которые особенно важны, – это теория вычислимости (ранее называемая теорией рекурсии), модальная логика и теория категорий. Теория вычислений основана на концепциях, определенных логиками и математиками, таких как Алонзо Черч и Алан Тьюринг. Черч впервые показал существование алгоритмически неразрешимых проблем, используя свое понятие лямбда-определимости. Тьюринг дал первый убедительный анализ того, что можно назвать механической процедурой, а Курт Гёдель утверждал, что он нашел анализ Тьюринга «идеальным». Кроме того, существуют и другие важные области теоретического пересечения логики и информатики: теорема о неполноте Гёделя доказывает, что любая логическая система, достаточно мощная для характеристики арифметики, будет содержать утверждения, которые нельзя ни доказать, ни опровергнуть в рамках этой системы. Это имеет непосредственное отношение к теоретическим вопросам, связанным с возможностью доказательства полноты и корректности программного обеспечения. Проблема фрейма – это фундаментальная проблема, которую необходимо решить при использовании логики первого порядка для представления целей агента искусственного интеллекта и состояния его окружения. Соответствие Карри — Ховарда – это связь между логическими системами и языками программирования. Эта теория установила точное соответствие между доказательствами и программами. В частности, она показала, что термы в просто типизированном лямбда-исчислении соответствуют доказательствам интуиционистской пропозициональной логики. Теория категорий представляет собой взгляд на математику, который подчеркивает отношения между структурами. Она тесно связана со многими аспектами информатики: системами типов для языков программирования, теорией систем переходов, моделями языков программирования и теорией семантики языков программирования. Логическое программирование – это парадигма программирования, баз данных и представления знаний, основанная на формальной логике. Логическая программа – это набор утверждений об определенной проблемной области. Вычисления выполняются путем применения логических рассуждений для решения задач в этой области. К основным семействам языков логического программирования относятся Prolog, Answer Set Programming (ASP) и Datalog.

Logic plays a fundamental role in computer science. Some of the key areas of logic that are particularly significant are computability theory (formerly called recursion theory), modal logic and category theory. The theory of computation is based on concepts defined by logicians and mathematicians such as Alonzo Church and Alan Turing. Church first showed the existence of algorithmically unsolvable problems using his notion of lambda definability. Turing gave the first compelling analysis of what can be called a mechanical procedure and Kurt Gödel asserted that he found Turing's analysis "perfect.". In addition some other major areas of theoretical overlap between logic and computer science are:
Gödel's incompleteness theorem proves that any logical system powerful enough to characterize arithmetic will contain statements that can neither be proved nor disproved within that system. This has direct application to theoretical issues relating to the feasibility of proving the completeness and correctness of software. The frame problem is a basic problem that must be overcome when using first order logic to represent the goals of an artificial intelligence agent and the state of its environment. The Curry–Howard correspondence is a relation between logical systems and programming languages. This theory established a precise correspondence between proofs and programs. In particular it showed that terms in the simply typed lambda calculus correspond to proofs of intuitionistic propositional logic. Category theory represents a view of mathematics that emphasizes the relations between structures. It is intimately tied to many aspects of computer science: type systems for programming languages, the theory of transition systems, models of programming languages and the theory of programming language semantics. Logic programming is a programming, database and knowledge representation paradigm that is based on formal logic. A logic program is a set of sentences about some problem domain. Computation is performed by applying logical reasoning to solve problems in the domain. Major logic programming language families include Prolog, Answer Set Programming (ASP) and Datalog.

Компьютеры в помощь логикам

Одним из первых приложений, использовавших термин «искусственный интеллект», была система «Логический теоретик», разработанная Алленом Ньюэллом, Клиффом Шоу и Гербертом Саймоном в 1956 году. Одной из задач логика является анализ набора логических утверждений и выведение заключений (дополнительных утверждений), которые должны быть истинными в соответствии с законами логики. Например, если даны утверждения «Все люди смертны» и «Сократ — человек», то логически верным заключением будет «Сократ смертен». Разумеется, это тривиальный пример. В реальных логических системах утверждения могут быть многочисленными и сложными. Уже на раннем этапе стало очевидно, что такой анализ может быть значительно упрощен с помощью компьютеров. Система «Логический теоретик» подтвердила теоретические работы Бертрана Рассела и Альфреда Норта Уайтхеда, изложенные в их влиятельном труде по математической логике «Principia Mathematica». Более того, последующие системы использовались логиками для проверки и открытия новых математических теорем и доказательств.

Логические приложения для компьютеров

Математическая логика всегда оказывала сильное влияние на область искусственного интеллекта (ИИ). С самого начала развития этой области стало понятно, что технологии автоматизации логических выводов обладают большим потенциалом для решения проблем и получения заключений из фактов. Рон Брахман описал логику первого порядка (FOL) как эталон, по которому следует оценивать все формализмы представления знаний в ИИ. Логика первого порядка – это общий и мощный метод описания и анализа информации. Причина, по которой сама FOL не используется в качестве компьютерного языка, заключается в том, что она избыточно выразительна, поскольку FOL позволяет легко формулировать утверждения, которые не сможет решить ни один компьютер, независимо от его мощности. Поэтому любая форма представления знаний в определенной степени представляет собой компромисс между выразительностью и вычислимостью. Чем выразительнее язык, тем ближе он к FOL, и тем выше вероятность, что он будет медленнее и подвержен бесконечному циклу. Например, правила IF–THEN, используемые в экспертных системах, аппроксимируют очень ограниченное подмножество FOL. Вместо произвольных формул с полным набором логических операторов, отправной точкой является то, что логики называют modus ponens. В результате, системы, основанные на правилах, могут поддерживать высокопроизводительные вычисления, особенно при использовании алгоритмов оптимизации и компиляции. С другой стороны, логическое программирование, сочетающее подмножество клауз Хорна логики первого порядка с немонотонной формой отрицания, обладает как высокой выразительной мощью, так и эффективными реализациями. В частности, язык логического программирования Prolog является языком программирования, полным по Тьюрингу. Datalog расширяет модель реляционной базы данных рекурсивными отношениями, а программирование на основе множеств ответов – это форма логического программирования, ориентированная на сложные (преимущественно NP-трудные) задачи поиска. Еще одна важная область исследований логической теории – это разработка программного обеспечения. Исследовательские проекты, такие как Knowledge Based Software Assistant и Programmer's Apprentice, применяют логическую теорию для проверки корректности спецификаций программного обеспечения. Они также используют логические инструменты для преобразования спецификаций в эффективный код для различных платформ и для доказательства эквивалентности между реализацией и спецификацией. Этот подход, основанный на формальных преобразованиях, часто требует значительно больше усилий, чем традиционная разработка программного обеспечения. Однако в определенных областях, с использованием подходящих формализмов и повторно используемых шаблонов, этот подход оказался жизнеспособным для коммерческих продуктов. К таким областям обычно относятся системы вооружения, системы безопасности и финансовые системы реального времени, где отказ системы может привести к чрезмерно высоким человеческим или финансовым потерям. Примером такой области является проектирование сверхбольших интегральных схем (VLSI) – процесс разработки чипов, используемых для процессоров и других критически важных компонентов цифровых устройств. Ошибка в чипе может быть катастрофической. В отличие от программного обеспечения, чипы нельзя исправить или обновить. Поэтому существует коммерческое обоснование для использования формальных методов для доказательства соответствия реализации спецификации. Другим важным применением логики в компьютерных технологиях является область языков фреймов и автоматических классификаторов. Языки фреймов, такие как KL ONE, могут быть непосредственно сопоставлены с теорией множеств и логикой первого порядка. Это позволяет специализированным решателям теорем, называемым классификаторами, анализировать различные объявления о множествах, подмножествах и отношениях в данной модели. Таким образом, модель можно проверить и выявить любые несогласованные определения. Классификатор также может выводить новую информацию, например, определять новые множества на основе существующей информации и изменять определения существующих множеств на основе новых данных. Такая гибкость идеально подходит для работы с постоянно меняющимся миром Интернета. Технология классификаторов строится на языках, таких как Web Ontology Language, для обеспечения логического семантического уровня поверх существующего Интернета. Этот слой называется Semantic Web. Временная логика используется для рассуждений в конкурентных системах.

There has always been a strong influence from mathematical logic on the field of artificial intelligence (AI). From the beginning of the field it was realized that technology to automate logical inferences could have great potential to solve problems and draw conclusions from facts. Ron Brachman has described first order logic (FOL) as the metric by which all AI knowledge representation formalisms should be evaluated. First order logic is a general and powerful method for describing and analyzing information. The reason FOL itself is simply not used as a computer language is that it is actually too expressive, in the sense that FOL can easily express statements that no computer, no matter how powerful, could ever solve. For this reason every form of knowledge representation is in some sense a trade off between expressivity and computability. The more expressive the language is, the closer it is to FOL, the more likely it is to be slower and prone to an infinite loop. For example, IF–THEN rules used in expert systems approximate to a very limited subset of FOL. Rather than arbitrary formulas with the full range of logical operators the starting point is simply what logicians refer to as modus ponens. As a result, rule based systems can support high performance computation, especially if they take advantage of optimization algorithms and compilation. On the other hand, logic programming, which combines the Horn clause subset of first order logic with a non monotonic form of negation, has both high expressive power and efficient implementations. In particular, the logic programming language Prolog is a Turing complete programming language. Datalog extends the relational database model with recursive relations, while answer set programming is a form of logic programming oriented towards difficult (primarily NP hard) search problems. Another major area of research for logical theory is software engineering. Research projects such as the Knowledge Based Software Assistant and Programmer's Apprentice programs have applied logical theory to validate the correctness of software specifications. They have also used logical tools to transform the specifications into efficient code on diverse platforms and to prove the equivalence between the implementation and the specification. This formal transformation driven approach is often far more effortful than traditional software development. However, in specific domains with appropriate formalisms and reusable templates the approach has proven viable for commercial products. The appropriate domains are usually those such as weapons systems, security systems, and real time financial systems where failure of the system has excessively high human or financial cost. An example of such a domain is Very Large Scale Integrated (VLSI) design—the process for designing the chips used for the CPUs and other critical components of digital devices. An error in a chip can be catastrophic. Unlike software, chips can't be patched or updated. As a result, there is commercial justification for using formal methods to prove that the implementation corresponds to the specification. Another important application of logic to computer technology has been in the area of frame languages and automatic classifiers. Frame languages such as KL ONE can be directly mapped to set theory and first order logic. This allows specialized theorem provers called classifiers to analyze the various declarations between sets, subsets, and relations in a given model. In this way the model can be validated and any inconsistent definitions flagged. The classifier can also infer new information, for example define new sets based on existing information and change the definition of existing sets based on new data. The level of flexibility is ideal for handling the ever changing world of the Internet. Classifier technology is built on top of languages such as the Web Ontology Language to allow a logical semantic level on top of the existing Internet. This layer is called the Semantic Web. Temporal logic is used for reasoning in concurrent systems.