Description logics form a family of knowledge representation languages for modeling ontologies. Model-finding is a technique for analyzing a first-order theory T by constructing and querying the models of T. This project develops a translation from description logic theories to first-order theories, enabling the use of the Razor model-finder. We provide an implementation of the translation algorithm, and a proof of correctness of the algorithm. As a case study, we explore a sample role-based access control policy formalized in description logic and show how to reason about using Razor.

• This report represents the work of one or more WPI undergraduate students submitted to the faculty as evidence of completion of a degree requirement. WPI routinely publishes these reports on its website without editorial or peer review.

Creator

• Murray, Nicholas Daniel
• Ford, Erica Danielle

Publisher

• Worcester Polytechnic Institute

Identifier

• E-project-043015-111746

Advisor

• Dougherty, Daniel J.

Year

• 2015

Date created

• 2015-04-30

Resource type

• Major Qualifying Project

Major

• Mathematical Sciences
• Interdisciplinary

Rights statement

• In Copyright

License

• All rights reserved