By their very design, many robot control programs are non-terminating. This paper describes a situation calculus approach to expressing and proving properties of non-terminating programs expressed in Golog, a high level logic programming language for modeling and implementing dynamical systems. Because in this approach actions and programs are represented in classical (second-order) logic, it is natural to express and prove properties of Golog programs, including non-terminating ones, in the very same logic. This approach to program proofs has the advantage of logical uniformity and the availability of classical proof theory.
Non-terminating processes in the situation calculus / De Giacomo, G.; Ternovska, E.; Reiter, R.. - In: ANNALS OF MATHEMATICS AND OF ARTIFICIAL INTELLIGENCE. - ISSN 1012-2443. - 88:5-6(2020), pp. 623-640. [10.1007/s10472-019-09643-9]
Non-terminating processes in the situation calculus
De Giacomo G.
;
2020
Abstract
By their very design, many robot control programs are non-terminating. This paper describes a situation calculus approach to expressing and proving properties of non-terminating programs expressed in Golog, a high level logic programming language for modeling and implementing dynamical systems. Because in this approach actions and programs are represented in classical (second-order) logic, it is natural to express and prove properties of Golog programs, including non-terminating ones, in the very same logic. This approach to program proofs has the advantage of logical uniformity and the availability of classical proof theory.| File | Dimensione | Formato | |
|---|---|---|---|
|
DeGiacomo_Non-terminating_2020.pdf
solo gestori archivio
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
406.24 kB
Formato
Adobe PDF
|
406.24 kB | Adobe PDF | Contatta l'autore |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
