دورية أكاديمية
أعرض في EDS

Converting ALC Connection Proofs into ALC Sequents

التفاصيل البيبلوغرافية
العنوان: Converting ALC Connection Proofs into ALC Sequents
المؤلفون: Eunice Palmeira, Fred Freitas, Jens Otten
المصدر: Electronic Proceedings in Theoretical Computer Science, Vol 301, Iss Proc. PxTP 2019, Pp 3-17 (2019)
بيانات النشر: Open Publishing Association, 2019.
سنة النشر: 2019
المجموعة: LCC:Mathematics
LCC:Electronic computers. Computer science
مصطلحات موضوعية: Mathematics, QA1-939, Electronic computers. Computer science, QA75.5-76.95
الوصف: The connection method has earned good reputation in the area of automated theorem proving, due to its simplicity, efficiency and rational use of memory. This method has been applied recently in automatic provers that reason over ontologies written in the description logic ALC. However, proofs generated by connection calculi are difficult to understand. Proof readability is largely lost by the transformations to disjunctive normal form applied over the formulae to be proven. Such a proof model, albeit efficient, prevents inference systems based on it from effectively providing justifications and/or descriptions of the steps used in inferences. To address this problem, in this paper we propose a method for converting matricial proofs generated by the ALC connection method to ALC sequent proofs, which are much easier to understand, and whose translation to natural language is more straightforward. We also describe a calculus that accepts the input formula in a non-clausal ALC format, what simplifies the translation.
نوع الوثيقة: article
وصف الملف: electronic resource
اللغة: English
تدمد: 2075-2180
Relation: http://arxiv.org/pdf/1908.09477v1; https://doaj.org/toc/2075-2180
DOI: 10.4204/EPTCS.301.3
URL الوصول: https://doaj.org/article/b3dadbd542ab4925bad46c4e82e2fc70
رقم الأكسشن: edsdoj.b3dadbd542ab4925bad46c4e82e2fc70
قاعدة البيانات: Directory of Open Access Journals
الوصف
تدمد:20752180
DOI:10.4204/EPTCS.301.3