Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sat, 8 Jan 1994 14:55:05 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26671; Sat, 8 Jan 1994 07:45:28 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA26667; Sat, 8 Jan 1994 07:45:16 -0700 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA05771; Sat, 8 Jan 1994 06:43:25 -0800 Received: from guillemot.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Sat, 8 Jan 1994 14:42:59 +0000 To: info-hol@cs.uidaho.edu Subject: HOL for lawyers? Date: Sat, 08 Jan 94 14:42:53 +0000 From: John Harrison Message-Id: <"swan.cl.cam.:233900:940108144314"@cl.cam.ac.uk> Reading the "Case Summaries" in the Independent newspaper (27th December 1993), I couldn't help noticing the following: `Since the object of ss 423 and 425 of the Insolvency Act 1986 was to remedy the avoidance of debts, the word "and" between paragraphs (a) and (b) of s 423(2) must be read conjunctively and not disjunctively.' This made me wonder if anyone has ever tried applying some sort of logical formalism in the specification of a human legal system, especially company law and tax law. It could do wonders for logicians' salaries. I'm sure Leibniz would have approved. John.