Student research opportunities
Are Election Laws Consistent?
Project Code: CECS_1106
This project is available at the following levels:
CS single semester, Honours, Summer Scholar, Masters, PhD
Keywords:
Non-Classical Logic, Law, Applied Logic
Supervisor:
Dr Dirk PattinsonOutline:
Laws are formulated in natural language, but need to be applied rigorously. One of the problem with the formalization of legal texts using logic is that there is no rule with exception. These exceptions can be elegantly treated using default implications that capture statements of the form "normally ..." and are implemented in the theorem prover "Cool" that is co-developed at ANU.
Goals of this project
The goal is to formalize parts of the ACT Electoral act that deal with vote counting under the Hare-Clark method. Given the formalization, consistency checking and classification should be applied to try and find inconsistencies or situations that are not dealt with in the act.
Requirements/Prerequisites
Interest in applied logic and some background in logical reasoning. No background in the specific logics used to formalize law is required.
Student Gain
Background and applications of logics in the real world, and potentially there's also a gain for the rest of the world by making laws more precise!
Background Literature
Not really background, but the procedure for vote counting in the ACT can be viewed at
http://www.legislation.act.gov.au/a/1992-71/default.asp
(vote counting is described in Schedule 4). The theorem prover is described in a sysem description at IJCAR 2014, available via
https://www8.cs.fau.de/~gorin/papers/ijcar14.pdf
