Published February 25, 2022 | Version v1
Publication

Automated Reasoning in Temporal DL-Lite

  • 1. Université Paris Cité
  • 2. National University of Comahue
  • 3. Free University of Bozen-Bolzano
  • 4. University of Bergen

Description

Automated Reasoning in Temporal DL-Lite* We investigate the feasibility of automated reasoning over temporal DL-Lite (TDL-Lite) knowledge bases (KBs). We translate TDL-Lite KBs into a fragment of First Order temporal logic and then into LTL, and apply off-the-shelf LTL and FO-based reasoners for checking the satisfiability. We conduct various experiments to analyse the size of the LTL translation as well as the runtime performance of different reasoners on toy scenarios and on randomly generated TDL-Lite KBs. To improve the reasoning performance when dealing with large ABoxes, our work also proposes an approach for abstracting temporal assertions in KBs. We run several experiments with this approach to assess the effectiveness of the technique by measuring the gain in terms of the size of the translation, and the number of both ABox assertions and individuals. We also measure the runtime of the solvers on such abstracted KBs. Lastly, in an effort to make the usage of TDL-Lite KBs a reality, we present a fully-fledged tool with a graphical interface to design and reason over them. Our interface is based on conceptual modeling principles and it is integrated with our translation tool and a temporal reasoner. (*) This work has been submitted to the Journal of Automated Reasoning

⚠️ This is an automatic machine translation with an accuracy of 90-95%

Translated Description (Arabic)

الاستدلال الآلي في DL - Lite الزمني * نحن نحقق في جدوى الاستدلال الآلي على قواعد المعرفة DL - Lite (TDL - Lite) الزمنية (KBs). نقوم بترجمة قواعد بيانات TDL - Lite إلى جزء من المنطق الزمني من الدرجة الأولى ثم إلى LTL، ونطبق المنطق الجاهز القائم على LTL و FO للتحقق من مدى الرضا. نجري تجارب مختلفة لتحليل حجم ترجمة LTL بالإضافة إلى أداء وقت التشغيل للمفكرين المختلفين في سيناريوهات الألعاب وعلى قاعدة المعارف TDL - Lite التي يتم إنشاؤها عشوائيًا. لتحسين أداء الاستدلال عند التعامل مع الصناديق الكبيرة، يقترح عملنا أيضًا نهجًا لتجريد التأكيدات الزمنية في قواعد المعلومات. نقوم بإجراء العديد من التجارب مع هذا النهج لتقييم فعالية التقنية من خلال قياس الكسب من حيث حجم الترجمة، وعدد كل من تأكيدات ABox والأفراد. نقيس أيضًا وقت تشغيل المحللين على قواعد المعلومات المستخلصة هذه. أخيرًا، في محاولة لجعل استخدام قواعد بيانات TDL - Lite حقيقة واقعة، نقدم أداة كاملة مع واجهة رسومية لتصميمها والتفكير فيها. تعتمد واجهتنا على مبادئ النمذجة المفاهيمية وهي متكاملة مع أداة الترجمة الخاصة بنا والمنطق الزمني. (*) تم تقديم هذا العمل إلى مجلة الاستدلال الآلي

Translated Description (French)

Raisonnement automatisé dans DL-Lite temporel * Nous étudions la faisabilité du raisonnement automatisé sur les bases de connaissances (KB) DL-Lite temporel (TDL-Lite). Nous traduisons les bases de connaissances TDL-Lite en un fragment de logique temporelle de premier ordre, puis en LTL, et appliquons des raisonneurs LTL et FO prêts à l'emploi pour vérifier la satisfiabilité. Nous menons diverses expériences pour analyser la taille de la traduction LTL ainsi que les performances d'exécution de différents raisonneurs sur des scénarios de jouets et sur des bases de données TDL-Lite générées de manière aléatoire. Pour améliorer la performance de raisonnement lorsqu'il s'agit de grands ABox, notre travail propose également une approche pour abstraire les assertions temporelles dans les KB. Nous menons plusieurs expériences avec cette approche pour évaluer l'efficacité de la technique en mesurant le gain en termes de taille de la traduction, et le nombre d'assertions ABox et d'individus. Nous mesurons également le temps d'exécution des solveurs sur ces bases de connaissances abstraites. Enfin, dans un effort pour faire de l'utilisation des bases de données TDL-Lite une réalité, nous présentons un outil à part entière avec une interface graphique pour les concevoir et les raisonner. Notre interface est basée sur des principes de modélisation conceptuelle et elle est intégrée à notre outil de traduction et à un raisonneur temporel. (*) Ce travail a été soumis au Journal of Automated Reasoning

Translated Description (Spanish)

Razonamiento automatizado en DL-Lite temporal * Investigamos la viabilidad del razonamiento automatizado sobre las bases de conocimiento (KB) de DL-Lite temporal (TDL-Lite). Traducimos las KB de TDL-Lite en un fragmento de lógica temporal de primer orden y luego en LTL, y aplicamos razonadores basados en LTL y FO listos para usar para verificar la satisfactibilidad. Realizamos varios experimentos para analizar el tamaño de la traducción LTL, así como el rendimiento en tiempo de ejecución de diferentes razonadores en escenarios de juguetes y en KB de TDL-Lite generados aleatoriamente. Para mejorar el rendimiento del razonamiento cuando se trata de grandes ABoxes, nuestro trabajo también propone un enfoque para abstraer afirmaciones temporales en KBs. Realizamos varios experimentos con este enfoque para evaluar la efectividad de la técnica midiendo la ganancia en términos del tamaño de la traducción y el número de afirmaciones e individuos de ABox. También medimos el tiempo de ejecución de los solucionadores en dichas bases de conocimientos abstraídas. Por último, en un esfuerzo por hacer realidad el uso de las bases de conocimientos de TDL-Lite, presentamos una herramienta completa con una interfaz gráfica para diseñar y razonar sobre ellas. Nuestra interfaz se basa en principios de modelado conceptual y está integrada con nuestra herramienta de traducción y un razonador temporal. (*) Este trabajo ha sido enviado al Journal of Automated Reasoning

Additional details

Additional titles

Translated title (Arabic)
الاستدلال الآلي في DL - Lite الزمني
Translated title (French)
Raisonnement automatisé dans Temporal DL-Lite
Translated title (Spanish)
Razonamiento automatizado en DL-Lite temporal

Identifiers

Other
https://openalex.org/W3049398720
DOI
10.5281/zenodo.6286971

GreSIS Basics Section

Is Global South Knowledge
Yes
Country
Argentina

References

  • https://openalex.org/W1489391022
  • https://openalex.org/W1516806823
  • https://openalex.org/W1524525494
  • https://openalex.org/W1548951066
  • https://openalex.org/W1549122259
  • https://openalex.org/W160269682
  • https://openalex.org/W1980167179
  • https://openalex.org/W2026807253
  • https://openalex.org/W2118791871
  • https://openalex.org/W2139125912
  • https://openalex.org/W2157319504
  • https://openalex.org/W233122475
  • https://openalex.org/W2402007929
  • https://openalex.org/W2513733182
  • https://openalex.org/W2740520395
  • https://openalex.org/W3003198512
  • https://openalex.org/W3024577520