Using first-order logic to reason about policies

It’s very hard to write good policies. For example, consider the following two policies `students may enter the student lab’ and `faculty members may not enter the student lab’.

They seem reasonable, but what should happen when a person who is both a student and a faculty member wants to enter the student lab? The problem with policies isn’t just that they might be inconsistent (although that’s bad enough!); they can be ambiguous too. For example, the policy `only administrators may edit the logs’ forbids people who are not administrators from editing the logs, but it isn’t clear if it says anything about the administrator’s rights. The goal of this project is to help policy makers write consistent, unambiguous policies. Also, we want to tell users what they may and may not do, as well as which policies grant or deny the rights.

To do this, we have found a fragment of first-order logic in which people can state and reason about policies. Because it’s first-order logic, there is no ambiguity. Furthermore, the analysis of the policies is provably correct. More specifically, we can prove in polynomial time whether or not the policies are consistent and whether or not they imply specific rights, such as allowing Alice to enter the student lab. We have a paper that explains all of this.

But, so what? Do you think anyone, but a logician is going to write policies in first-order logic? Of course not. So, what we need is an interface that smart, non-logicians can use to write policies and ask questions about them. The idea is that their policies and questions are translated to the first-order language, analyzed, and the answers to their questions returned in a language that they can understand, namely English. At this point, we have preliminary drawings of what the interface may look like, along with the appropriate translation to (and from) the logic. What we need are one to two students who are willing to do a little design work, a fair amount of creative programming to do the policy analysis, and a lot of clean coding with Java swing components to make the interface. Once the work is done, librarians will review the prototype and judge if the approach could really work for them. This project is likely to lead to a publication and there is a possibility that it will become part of Fedora (and, thus, become a significant piece of work towards the creation of large-scale digital libraries).

Contact: To discuss the project, please email Vicky Weissman, vickyw@cs.cornell.edu.