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:<p><pre><code>   (define ([Person]X is-thief of: [Property]P belonging-to: [Person]Y)
      (and
         (X appropriates P)
         (X != Y)
         (X intends 
            ((Time&#62;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")
</code></pre>
There could then be a compiler and other software to automatically reason about such statements.