An optimal construction of Hanf sentences |
| |
| Authors: | Benedikt Bollig Dietrich Kuske |
| |
| Affiliation: | 1. Laboratoire Spécification et Vérification, École Normale Supérieure de Cachan & Centre National de la Recherche Scientifique, France;2. Institut für Theoretische Informatik, TU Ilmenau, Germany |
| |
| Abstract: | We give a new construction of formulas in Hanf normal form that are equivalent to first-order formulas over structures of bounded degree. This is the first algorithm whose running time is shown to be elementary. The triply exponential upper bound is complemented by a matching lower bound. |
| |
| Keywords: | |
| 本文献已被 ScienceDirect 等数据库收录！ |
