This is a case-study in knowledge representation. We analyze the ‘one hundred prisoners and a lightbulb’ puzzle. In this puzzle it is relevant what the agents (prisoners) know...
In 1926, Mally proposed the first formal deontic system. As Mally and others soon realized, this system had some rather strange consequences. We show that the strangeness of Mally...
The aim of this paper is to strengthen the point made by Horty about the relationship between reason holism and moral particularism. In the literature prima facie obligations have ...
Abstract. We show that a recently developed theory of positive permission based on the notion of derogation is hampered by a triviality result that indicates a problem with the und...
Compliance is often achieved ‘by design’ through a coherent system of controls consisting of information systems and procedures . This system-based control requires a new appro...
Brigitte Burgemeestre, Joris Hulstijn, Yao-Hua Tan
Abstract. Privacy policies are often defined in terms of permitted messages. Instead, in this paper we derive dynamically the permitted messages from static privacy policies defi...
Guillaume Aucher, Guido Boella, Leendert van der T...
Abstract. This paper describes a formalization of the weakest precondition, wp, for general recursive programs using the type-theoretical proof assistant Coq. The formalization is ...
Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu
In this paper we introduce a new approach to axiomatizing quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a speci...
We describe the operational and denotational semantics of a small imperative language in type theory with inductive and recursive definitions. The operational semantics is given b...