A Step Up in Expressiveness of Decidable Fixpoint Logics

Benedikt, Michael; Bourhis, Pierre; Vanden Boom, Michael

Type de document :

Communication dans un congrès avec actes

Titre :

A Step Up in Expressiveness of Decidable Fixpoint Logics

Auteur(s) :

Benedikt, Michael [Auteur]
Computing Science Laboratory - Oxford University
Bourhis, Pierre [Auteur]

Linking Dynamic Data [LINKS]
Vanden Boom, Michael [Auteur]
Computing Science Laboratory - Oxford University

Titre de la manifestation scientifique :

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

Ville :

New York

Pays :

Etats-Unis d'Amérique

Date de début de la manifestation scientifique :

2016-07-05

Discipline(s) HAL :

Informatique [cs]/Intelligence artificielle [cs.AI]

Résumé en anglais : [en]

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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Fichiers

https://hal.inria.fr/hal-01413890/document
Accès libre
Accéder au document

https://hal.inria.fr/hal-01413890/document
Accès libre
Accéder au document

https://hal.inria.fr/hal-01413890/document
Accès libre
Accéder au document

document
Accès libre
Accéder au document

LICS16-gnfpup-long.pdf
Accès libre
Accéder au document

A Step Up in Expressiveness of Decidable ... BibTeX CSV Excel RIS

Fichiers

A Step Up in Expressiveness of Decidable ...

BibTeX

CSV

Excel

RIS