Guarded Successor: A Novel Temporal Logic
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909247155994624 |
|---|---|
| author | Asor, Ohad |
| author_facet | Asor, Ohad |
| contents | We present GS (Guarded Successor), a novel decidable temporal logic with several unique distinctive features. Among those, it allows infinitely many data values that come not only with equality but with a somehow rich theory too: the first-order theory of atomless Boolean algebras. The language also distinguishes between inputs and outputs, and has a decision procedure for determining whether for all inputs exist outputs, at each point of time. Moreover, and maybe most surprisingly, the data values can be nothing but sentences in GS itself. We also present a non-temporal fragment called NSO (Nullary Second Order) that enjoys merely this last property. These results are crucial necessary ingredients in any meaningful design of safe AI. Finally, all those results are obtained from a novel treatment of the first-order theory of atomless Boolean algebras. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_06214 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Guarded Successor: A Novel Temporal Logic Asor, Ohad Logic in Computer Science Logic We present GS (Guarded Successor), a novel decidable temporal logic with several unique distinctive features. Among those, it allows infinitely many data values that come not only with equality but with a somehow rich theory too: the first-order theory of atomless Boolean algebras. The language also distinguishes between inputs and outputs, and has a decision procedure for determining whether for all inputs exist outputs, at each point of time. Moreover, and maybe most surprisingly, the data values can be nothing but sentences in GS itself. We also present a non-temporal fragment called NSO (Nullary Second Order) that enjoys merely this last property. These results are crucial necessary ingredients in any meaningful design of safe AI. Finally, all those results are obtained from a novel treatment of the first-order theory of atomless Boolean algebras. |
| title | Guarded Successor: A Novel Temporal Logic |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2407.06214 |