A Step Up in Expressiveness of Decidable ...
Document type :
Communication dans un congrès avec actes
Title :
A Step Up in Expressiveness of Decidable Fixpoint Logics
Author(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
Computing Science Laboratory - Oxford University
Bourhis, Pierre [Auteur]
Linking Dynamic Data [LINKS]
Vanden Boom, Michael [Auteur]
Computing Science Laboratory - Oxford University
Conference title :
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
City :
New York
Country :
Etats-Unis d'Amérique
Start date of the conference :
2016-07-05
HAL domain(s) :
Informatique [cs]/Intelligence artificielle [cs.AI]
English abstract : [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 ...
Show more >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.Show less >
Show more >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.Show less >
Language :
Anglais
Peer reviewed article :
Oui
Audience :
Internationale
Popular science :
Non
Collections :
Source :
Files
- https://hal.inria.fr/hal-01413890/document
- Open access
- Access the document
- https://hal.inria.fr/hal-01413890/document
- Open access
- Access the document
- https://hal.inria.fr/hal-01413890/document
- Open access
- Access the document
- document
- Open access
- Access the document
- LICS16-gnfpup-long.pdf
- Open access
- Access the document