A step up in expressiveness of decidable fixpoint logics
Guardedness restrictions are one of the principal means to obtain decidable logics — operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while re...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Published: |
Association for Computing Machinery
2016
|
| _version_ | 1797105694612127744 |
|---|---|
| author | Boom, M Benedikt, M Bourhis, P |
| author_facet | Boom, M Benedikt, M Bourhis, P |
| author_sort | Boom, M |
| collection | OXFORD |
| description | Guardedness restrictions are one of the principal means to obtain decidable logics — operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic. |
| first_indexed | 2024-03-07T06:51:00Z |
| format | Conference item |
| id | oxford-uuid:fc8d0e38-b874-4bf5-ade5-b4294941a9a8 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:51:00Z |
| publishDate | 2016 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:fc8d0e38-b874-4bf5-ade5-b4294941a9a82022-03-27T13:21:39ZA step up in expressiveness of decidable fixpoint logicsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:fc8d0e38-b874-4bf5-ade5-b4294941a9a8Symplectic Elements at OxfordAssociation for Computing Machinery2016Boom, MBenedikt, MBourhis, PGuardedness restrictions are one of the principal means to obtain decidable logics — operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic. |
| spellingShingle | Boom, M Benedikt, M Bourhis, P A step up in expressiveness of decidable fixpoint logics |
| title | A step up in expressiveness of decidable fixpoint logics |
| title_full | A step up in expressiveness of decidable fixpoint logics |
| title_fullStr | A step up in expressiveness of decidable fixpoint logics |
| title_full_unstemmed | A step up in expressiveness of decidable fixpoint logics |
| title_short | A step up in expressiveness of decidable fixpoint logics |
| title_sort | step up in expressiveness of decidable fixpoint logics |
| work_keys_str_mv | AT boomm astepupinexpressivenessofdecidablefixpointlogics AT benediktm astepupinexpressivenessofdecidablefixpointlogics AT bourhisp astepupinexpressivenessofdecidablefixpointlogics AT boomm stepupinexpressivenessofdecidablefixpointlogics AT benediktm stepupinexpressivenessofdecidablefixpointlogics AT bourhisp stepupinexpressivenessofdecidablefixpointlogics |