An extension of Horn clause logic is defined based on the introduction of a synchronization operator. Generalized Horn clauses (GHC) are introduced through an informal description of their operational semantics, which allows discussion of some typical synchronization problems. GHC are first considered formally as a programming language by defining the syntax, the operational semantics, the model-theoretic semantics, and the fixed-point semantics. The above mentioned semantics are given in the Van Emden-Kowalski style (1976, J. Assoc. Comput. Mach. 23, 733–742) and are proved equivalent. GHC are then characterized as axiomatic theories. A set of axiom schemata concerned with the newly introduced synchronization operator is defined and it is proved that the operational semantics inference rule is both sound and complete. Finally, the relation between GHC and Horn clauses is analyzed, and it is proved that Horn clause logic is strictly included in the generalized Horn clause logic.
Scheda prodotto non validato
Scheda prodotto in fase di analisi da parte dello staff di validazione
|Titolo:||A Synchronization Logic: Axiomatics and FormalSemantics of Generalized Horn Clauses|
|Rivista:||INFORMATION AND CONTROL|
|Citazione:||Falaschi, M., Levi, G., Martelli, M., & Palamidessi, C. (1984). A Synchronization Logic: Axiomatics and FormalSemantics of Generalized Horn Clauses. INFORMATION AND CONTROL, 60(1), 36-69.|
|Appare nelle tipologie:||1.1 Articolo in rivista|
File in questo prodotto: