A formal logic framework for the automation of the right to be forgotten

Abstract

The right to be forgotten results from a ruling of the European Court of Justice. It empowers individuals to control the display of their personal data indexed by a search engine. Specifically, it requires Internet search engine operators to deploy a process for individuals to file requests concerning the removal of their personal data from search indices. To support the right to be forgotten, search engine operators such as Google, Microsoft and Yahoo currently provide a web form where users submit all relevant information. A subsequent manual process by the search engine operators assesses whether the author of the request is eligible to exercise the right to be forgotten and if the request itself is lawful. However, manual verification is inefficient, unscalable, and prone to subjective judgment. A framework for automated reasoning about case law (“PriCL”) could in principle tell whether some precedents lead to the conclusion that some action is legal or illegal. However, PriCL leverages first order logic, and hence, is insufficient to determine similarity of cases. In this paper, we design a framework that extends PriCL’s logic with similarity measures in order to automate the enforcement of the right to be forgotten. Our implementation of this logic leverages the Z3 theorem prover. We evaluate the framework by performing 10 case studies on the right to be forgotten. Each case was decided correctly in less than 1s.