While researchers are becoming to appreciate the natural connections between law and computer science, the number of courses where students can learn about logic, law, and automated reasoning are few. Even Yale University, which is traditionally oriented towards humanities- and law-related disciplines, has never had such a course. In Fall 2022 semester, Professor Piskac (Yale CS Department) and Professor Shapiro (Yale Law School) jointly taught "Law, Security, and Logic” for the first time. The student body was diverse, both in terms of their declared majors, as well as race and gender. Few students had encountered techniques of automated reasoning or legal reasoning.

This talk will report on our experiences in teaching this course. The course was a combination of traditional lectures and application-type work. The course instructors gave lectures covering the basic themes, such as first-order logic, automated reasoning, SMT solvers, legal reasoning, and legal interpretation. The students also got hands-on experience: they used existing automated reasoning tools to model real-world protocols and show their correctness or detect vulnerabilities.

Moreover, students used automated reasoning tools to check regulatory compliance automatically. There are many statutes and regulations that are a challenge to understand, even for experts. The Foreign Intelligence Surveillance Act of 1978 (FISA) is a prime example. FISA is the main authorization for foreign intelligence collection in the United States. It is an extremely important statute and our students were intensely interested in it, as it regulates domestic surveillance of the internet. Unfortunately, FISA is an extremely complicated statute. Evidence even suggests that it was intentionally drafted to obfuscate its meaning. Entire courses in law school are devoted to it. In the class, the students used first-order logic to formulate the definition of electronic surveillance as set out in 50 USC 1801(f). They automatically checked various scenarios to determine whether they would be considered “electronic surveillance” under FISA.

Based on this class, we believe that formal automated reasoning can be applied to legal topics, such as formalizing norms used in privacy policy regulations, legal rental contracts, or property law, just to name a few, which are the standard topics considered in this workshop, and can be taught to undergraduate CS majors.

We will conclude this talk with suggestions about additional research directions that combine legal and automated reasoning. In particular, we will describe our ongoing project on using counterfactual reasoning for legal accountability, as well as using formal methods to exploit legal code.