Something a bit like Prolog might do the job. There would also have to be terminal predicates coded in English. So theft (in English law defined as: "dishonestl

Something a bit like Prolog might do the job. There would also have to be terminal predicates coded in English. So theft (in English law defined as: "dishonestly appropriat[ing] property belonging to another with the intention of permanently depriving the other of it") might be: (define ([Person]X is-thief of: [Property]P belonging-to: [Person]Y) (and (X appropriates P) (X != Y) (X intends ((Time>now) implies not (Y has P))) (dishonestly))) (define dishonestly "this is purposely left undefined in the law") (define ([Person]X appropriates [Property]P) "X does some action causing him to have control over P") There could then be a compiler and other software to automatically reason about such statements.