Converting ALC Connection Proofs into ALC Sequents

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 gen...

Full description

Bibliographic Details
Main Authors: Eunice Palmeira, Fred Freitas, Jens Otten
Format: Article
Language:English
Published: Open Publishing Association 2019-08-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1908.09477v1