A goal-directed decision procedure for hybrid PDL
<p>We present the first goal-directed decision procedure for hybrid PDL. The procedure is based on a modular approach that scales from basic modal logic with eventualities to hybrid PDL. The approach is designed so that nominals and eventualities are treated orthogonally. To deal with the comp...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Springer Netherlands
2014
|
| Subjects: |
| _version_ | 1797068754842025984 |
|---|---|
| author | Kaminski, M Smolka, G |
| author_facet | Kaminski, M Smolka, G |
| author_sort | Kaminski, M |
| collection | OXFORD |
| description | <p>We present the first goal-directed decision procedure for hybrid PDL. The procedure is based on a modular approach that scales from basic modal logic with eventualities to hybrid PDL. The approach is designed so that nominals and eventualities are treated orthogonally. To deal with the complex programs of PDL, the approach employs a novel disjunctive program decomposition. In arguing the correctness of our approach, we employ the novel notion of support generalizing the standard notion of Hintikka sets.</p> |
| first_indexed | 2024-03-06T22:14:39Z |
| format | Journal article |
| id | oxford-uuid:52fba724-fb6a-4322-a83f-7b25efa83afb |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T22:14:39Z |
| publishDate | 2014 |
| publisher | Springer Netherlands |
| record_format | dspace |
| spelling | oxford-uuid:52fba724-fb6a-4322-a83f-7b25efa83afb2022-03-26T16:28:51ZA goal-directed decision procedure for hybrid PDLJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:52fba724-fb6a-4322-a83f-7b25efa83afbModal logicEnglishOxford University Research Archive - ValetSpringer Netherlands2014Kaminski, MSmolka, G<p>We present the first goal-directed decision procedure for hybrid PDL. The procedure is based on a modular approach that scales from basic modal logic with eventualities to hybrid PDL. The approach is designed so that nominals and eventualities are treated orthogonally. To deal with the complex programs of PDL, the approach employs a novel disjunctive program decomposition. In arguing the correctness of our approach, we employ the novel notion of support generalizing the standard notion of Hintikka sets.</p> |
| spellingShingle | Modal logic Kaminski, M Smolka, G A goal-directed decision procedure for hybrid PDL |
| title | A goal-directed decision procedure for hybrid PDL |
| title_full | A goal-directed decision procedure for hybrid PDL |
| title_fullStr | A goal-directed decision procedure for hybrid PDL |
| title_full_unstemmed | A goal-directed decision procedure for hybrid PDL |
| title_short | A goal-directed decision procedure for hybrid PDL |
| title_sort | goal directed decision procedure for hybrid pdl |
| topic | Modal logic |
| work_keys_str_mv | AT kaminskim agoaldirecteddecisionprocedureforhybridpdl AT smolkag agoaldirecteddecisionprocedureforhybridpdl AT kaminskim goaldirecteddecisionprocedureforhybridpdl AT smolkag goaldirecteddecisionprocedureforhybridpdl |