Skip to main content

A Polynomial Translation from the Two−Variable Guarded Fragment with Number Restrictions to the Guarded Fragment.

Yevgeny Kazakov

Abstract

We consider a two-variable guarded fragment with number restrictions for binary relations and give a satisfiability preserving transformation of formulas in this fragment to the three-variable guarded fragment. The translation can be computed in polynomial time and produces a formula that is linear in the size of the initial formula even for the binary coding of number restrictions. This allows one to reduce reasoning problems for many description logics to the satisfiability problem for the guarded fragment

Book Title
JELIA
Pages
372−384
Publisher
Springer
Series
Lecture Notes in Computer Science
Volume
3229
Year
2004