A Near-optimal Method for Reasoning About Action
We give an algorithm for "before-after" reasoning about action. The algorithm decides satisfiability and validity of formulae of propositional dynamic logic, a recently developed logic of change of state that subsumes the zero-order component of most other action-oriented logics. The algor...
| Main Author: | |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/148941 |
| _version_ | 1826193359166767104 |
|---|---|
| author | Pratt, Vaughan R. |
| author_facet | Pratt, Vaughan R. |
| author_sort | Pratt, Vaughan R. |
| collection | MIT |
| description | We give an algorithm for "before-after" reasoning about action. The algorithm decides satisfiability and validity of formulae of propositional dynamic logic, a recently developed logic of change of state that subsumes the zero-order component of most other action-oriented logics. The algorithm requires time at most proportional to an exponentially growing function of the length (number of occurences of variabes and connectives) of the input. Fischer and Ladner have shown that that every algorithm for this problem must take exponential time, making this algorithm optimal to within a polynomial. No decision method for any other logic is known to be optimal to within less than an expoential. The typical time for our algorithm makes it a heuristically efficient algorithm of considerable pratical interest. Application areas incluse program verification, program synthesis, and discourse analysis. The algorithm is based on the method of semantic tableaux, appropriately generalized to dynamic logic. A novel treatment of Hintikka sets via theory algebras supplies the theoretical basis for our treatment of tableaux. |
| first_indexed | 2024-09-23T09:37:48Z |
| id | mit-1721.1/148941 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T09:37:48Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1489412023-03-30T04:09:58Z A Near-optimal Method for Reasoning About Action Pratt, Vaughan R. We give an algorithm for "before-after" reasoning about action. The algorithm decides satisfiability and validity of formulae of propositional dynamic logic, a recently developed logic of change of state that subsumes the zero-order component of most other action-oriented logics. The algorithm requires time at most proportional to an exponentially growing function of the length (number of occurences of variabes and connectives) of the input. Fischer and Ladner have shown that that every algorithm for this problem must take exponential time, making this algorithm optimal to within a polynomial. No decision method for any other logic is known to be optimal to within less than an expoential. The typical time for our algorithm makes it a heuristically efficient algorithm of considerable pratical interest. Application areas incluse program verification, program synthesis, and discourse analysis. The algorithm is based on the method of semantic tableaux, appropriately generalized to dynamic logic. A novel treatment of Hintikka sets via theory algebras supplies the theoretical basis for our treatment of tableaux. 2023-03-29T14:11:13Z 2023-03-29T14:11:13Z 1978-09 https://hdl.handle.net/1721.1/148941 4846778 MIT-LCS-TM-113 application/pdf |
| spellingShingle | Pratt, Vaughan R. A Near-optimal Method for Reasoning About Action |
| title | A Near-optimal Method for Reasoning About Action |
| title_full | A Near-optimal Method for Reasoning About Action |
| title_fullStr | A Near-optimal Method for Reasoning About Action |
| title_full_unstemmed | A Near-optimal Method for Reasoning About Action |
| title_short | A Near-optimal Method for Reasoning About Action |
| title_sort | near optimal method for reasoning about action |
| url | https://hdl.handle.net/1721.1/148941 |
| work_keys_str_mv | AT prattvaughanr anearoptimalmethodforreasoningaboutaction AT prattvaughanr nearoptimalmethodforreasoningaboutaction |