Modular Reasoning in Isabelle

2000 ◽  
pp. 99-114 ◽  
Author(s):  
Florian Kammüller
Keyword(s):  
Modular Reasoning

Modular reasoning about concurrent higher-order imperative programs

2014 ◽  
Vol 49 (1) ◽  
pp. 1-1
Author(s):  
Lars Birkedal
Keyword(s):  
Higher Order ◽  
Modular Reasoning

Modular reasoning about structured TLA specifications

1999 ◽  
pp. 217-229 ◽  
Author(s):  
Georg Rock ◽  
Werner Stephan ◽  
Andreas Wolpers
Keyword(s):  
Modular Reasoning

Autonomous Agents Adopting Organizational Rules

2009 ◽  
pp. 314-333 ◽  
Author(s):  
Bob van der Vecht ◽  
Frank Dignum ◽  
John-Jules Ch. Meyer
Keyword(s):  
Autonomous Agents ◽  
Event Processing ◽  
Modular Approach ◽  
Organizational Models ◽  
Bottom Up ◽  
Organizational Goals ◽  
Reasoning Process ◽  
Modular Reasoning ◽  
Organizational Rules

This chapter discusses how autonomous agents can adopt organizational rules into their reasoning process. Agents in an organization need to coordinate their actions in order to reach the organizational goals. Organizational models specify the desired behaviour in terms of roles, relations, norms, and interactions. We have developed a method to translate norms into event-processing rules of the agents. We propose a modular reasoning model that includes the organizational rules explicitly. Since the agents are autonomous, they will have their own reasoning rules next to the organizational rules. The modular approach allows for meta-reasoning about these rules. We show that this stimulates bottom-up dynamics in the organization.

scholarly journals A step-indexed Kripke model of hidden state

2012 ◽  
Vol 23 (1) ◽  
pp. 1-54 ◽  
Author(s):  
JAN SCHWINGHAMMER ◽  
LARS BIRKEDAL ◽  
FRANÇOIS POTTIER ◽  
BERNHARD REUS ◽  
KRISTIAN STØVRING ◽  
...  
Keyword(s):  
Metric Space ◽  
Possible Worlds ◽  
Operational Semantics ◽  
Kripke Model ◽  
The State ◽  
Local State ◽  
Modular Reasoning ◽  
Proof Rules ◽  
Model Based ◽  
First Sound

Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from the context.We discuss the semantic foundations of frame and anti-frame rules, and present the first sound model for Charguéraud and Pottier's type and capability system including both of these rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are given by a recursively defined metric space. We also extend the model to account for Pottier's generalised frame and anti-frame rules, where invariants are generalised to families of invariants indexed over preorders. This generalisation enables reasoning about some well-bracketed as well as (locally) monotone uses of local state.

Sign in / Sign up

Export Citation Format

Share Document