You are here
Are Election Laws Consistent?
Research areas
Temporary Supervisor
Description
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
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
Interest in applied logic and some background in logical reasoning. No background in the specific logics used to formalize law is required.
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/defaul... (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
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!
