Search

Eines der Ziele künstlicher Intelligenz ist die Fähigkeit, Probleme durch Lernen und automatische Deduktion zu lösen. Bekannte Beispiele intelligenter Systeme sind in Chemie und Spielen wie Schach und Go zu finden. Die aktuell erfolgreichsten Ansätze in diesen Bereichen kombinieren Suchstrategien mit von maschinellen Lernmethoden gelernten statistischen Modellen. Allerdings involvieren mathematische Probleme abstraktere Prinzipien wie Induktion, die automatisierte logische Deduktion erschweren. Der Beweis neuer Theoreme erfordert häufig die Ausnutzung von Mustern, die in komplexen Strukturen eingebettet sind. Das Ziel unseres Projektes ist die Verbesserung automatischer Beweissuchmethoden in der Mathematik. Diese ermöglicht die Reduktion der Zeit, die zum formalen Beweisen komplexer Theoreme wie der Keplerschen Vermutung benötigt wird. Um unser System von einer großen Menge an Beispielen lernen zu lassen, identifizieren wir ähnliche Konzepte in verschiedenen formellen Bibliotheken von interaktiven Theorembeweisern (ITP). Das kombinierte Wissen wird von einem statistischen Modell verarbeitet, welches Beziehungen zwischen mathematischen Objekten ableitet. Wir nutzen diese Beziehungen aus, um bessere Strategien zum Beweis von Theoremen zu erzeugen. Unser System kombiniert Wissen von ITPs mit der Suchfähigkeit von automatischen Theorembeweisern (ATPs). Dies erlaubt es, die Beziehung zwischen neuen Vermutungen und vorhergegangenem formalisierten Wissen mittels des statistischen Modells zu verstehen. Unser System wählt für den Beweis einer Vermutung relevante Theoreme aus, vereinfacht den Beweis durch die Annahme von Lemmata und lenkt die Beweissuche durch den Vorschlag von erfolgversprechenden Beweisschritten. Wenn das System erfolgreich ist, erzeugt es einen automatisch verifizierten Beweis der Vermutung., One of the aims of artificial intelligence is to be able to solve problems through learning and automated reasoning. Famous examples of intelligent systems can be found in molecular chemistry and games such as chess and Go. The current most successful approaches in these domains combine statistical models trained by machine learning methods with search strategies. However, more abstract problems, generally out of reach of current methods, constructed from abstract principles such as induction appear commonly in mathematics. And proving new theorems often requires to exploit patterns hidden in complex structures. The aim of this thesis is to improve automated reasoning techniques in mathematics. This would help to reduce the time needed for formally proving complex theorems such as the Kepler conjecture. In order for our system to learn from a large number of examples, we align the formal libraries of interactive theorem provers (ITPs) by recognizing similar concepts. The shared knowledge is processed by a statistical model which infers relations between mathematical objects. We exploit those links to produce better strategies for proving theorems. In practice, our project combines ITP knowledge with the search power of automated theorem provers (ATPs). Therefore, if a mathematician states a conjecture in an ITP, our system understands through the statistical model the relation of the conjecture to previously formalized knowledge. It selects theorems relevant for proving the conjecture, simplifies the proof by conjecturing intermediate lemmas and may also guide the proof search by choosing suitable reasoning methods. If successful, it produces a computer- verified proof of the conjecture., by Thibault Gauthier, Kumulative Dissertation aus sechs Artikeln, in deutscher und französischer Sprache, University of Innsbruck, Dissertation, 2018, OeBB, (VLID)2759666

Purpose. The paper is aimed to analyze the functioning of the existing railway informational system, as the data storage, consideration of the ways to changeover to intelligent management system, including the application of semantic approach. It is necessary to change the paradigm of automated traffic management; this determines changing the paradigm in railway operation management. The development and introduction of new Business-Intelligence-type system requires the formalized knowledge on railway transportation process to be implemented, including in the form of ontology as the model and means to formalize the knowledge. New knowledge requires using the terms and concepts to describe the new processes and management objects in railway operations. Methodology. Formalizing the knowledge one should abstract away from classical definitions such as marshaling or freight station, train station, division station, dead-end station, railway junction, railway hub etc. Unified Modeling Languages for engineering the automated systems use the definitions: the objects’ categories, the class diagrams, statechart diagrams, sequence diagrams, activity diagrams, component diagrams, link diagrams in properties etc. These concepts enable formalizing the knowledge, bringing to homogeneous representing and using them for modeling the management processes of goods delivery. Findings. The data on timing the events of goods delivery process, breakings of schedule are taken into account in set-theoretical model on scripting scenarios for goods delivery process. One of the concepts in the model on breaking of schedule (from the knowledge base of the system ASK VPUZ-E enables to take into account the influence of possible factors and the real railway operations conditions. Originality. The ways to formalize knowledge on railway transportation process as the major premise to form intelligent informational software for management system were analyzed. The set-theoretical models on goods deli, Цель. Научная работа имеет своей целью анализ функционирования существующей информационной системы железной дороги, как хранилища данных, и рассмотрение путей перехода к интеллектуальной системе управления, в т. ч. с использованием семантического подхода. Сейчас необходима смена парадигмы автоматизированного управления перевозками, что обусловливает изменение модели управления эксплуатационной работой железной дороги. Для разработки и внедрения новой системы класса BusinessIntelligence необходимо создание формализованных знаний о перевозочном процессе железной дороги, в том числе в виде онтологий, как модели и средства формализации знаний. Новые знания нуждаются в использовании терминов и понятий, отражающих новые процессы и объекты управления в эксплуатационной работе. Методика. При формализации знаний необходимо абстрагироваться от классических определений, таких как сортировочная, грузовая, техническая или участковая станции, железнодорожный узел, развитой железнодорожный узел и т. п. Унифицированные языки моделирования для проектирования автоматизированных систем используют понятия: категории объектов, диаграммы классов, сословий, последовательности, деятельности, компонентов, отношений между свойствами. Эти понятия позволяют формализовать знания, привести к однотипным представлениям и использовать их для моделирования процессов управления доставкой груза. Результаты. Данные о времени совершения событий процесса доставки груза, отклонения в плане-графике учитываются в теоретико-множественной модели сценариев процесса доставки. Один из концептов модели отклонения от плана (с базы знаний системы АСК ВП УЗ–Е) позволяет учесть влияние возможных факторов и условия реальной эксплуатационной работы. Научная новизна. Рассмотрены пути формализации знаний о перевозочном процессе как предпосылки формирования интеллектуального информационного обеспечения системы управления. Построены теоретико-множественные модели управления доставкой груза для составления сценариев процесс, Мета. Наукова робота має за мету аналіз функціонування існуючої інформаційної системи залізниці,як сховища даних, та розгляд шляхів переходу до інтелектуальної системи управління,у т. ч. з використанням семантичного підходу. Наразі необхідна зміна парадигми автоматизованого управління перевезеннями, що обумовлює зміну моделі управління експлуатаційною роботою залізниці. Для розробки та впровадження нової системи класу Business Intelligence необхідне створення формалізованих знаньпро перевізний процес залізниці, у т. ч. у вигляді онтологій, як моделі та засобу формалізації знань.Нові знання потребують використання термінів та понять, що відображають нові процеси та об’єкти управління в експлуатаційній роботі. Методика. При формалізації знань необхідно абстрагуватись від класичних визначень, таких як сортувальна, вантажна, технічна або дільнична станції, залізничний вузол, розвинений залізничний вузол і т. ін. Уніфіковані мови моделювання для проектування автоматизованих систем використовують поняття: категорії об’єктів, діаграми класів, станів, послідовності, діяльності, компонентів, відношень між властивостями тощо. Ці поняття дозволяють формалізувати знання, привести до однотипних представлень та використовувати їх для моделювання процесів управління доставкою вантажу. Результати. Дані про час здійснення подій процесу доставки вантажу, відхилення у плані-графіку враховуються в теоретико-множинній моделі сценаріїв процесу доставки. Один із концептів моделі відхилення від плану (з бази знань системи АСКВПУЗ–Є) дозволяє врахувати вплив можливих факторів та умови реальної експлуатаційної роботи. Наукова новизна. Розглянуті шляхи формалізації знань про перевізний процес як передумови формування інтелектуального інформаційного забезпечення системи управління. Побудовано теоретико-множинні моделі управління доставкою вантажу для складання сценаріїв процесу доставки, наведені приклади використання засобів об’єктно-орієнтованого моделювання для алгоритмізації технологічних