Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (actually mcs.anl.gov !OR! owner-qed@mcs.anl.gov) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 18 May 1995 19:44:36 +0100 Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10) id NAA19937 for qed-out; Thu, 18 May 1995 13:35:22 -0500 Received: from catseye.idbsu.edu (catseye.idbsu.edu [132.178.200.125]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP id NAA19932 for ; Thu, 18 May 1995 13:35:16 -0500 Message-Id: <199505181835.NAA19932@antares.mcs.anl.gov> Received: by catseye.idbsu.edu (1.38.193.4/16.2) id AA05430; Thu, 18 May 1995 12:39:59 -0600 Date: Thu, 18 May 1995 12:39:59 -0600 From: Randall Holmes To: qed@mcs.anl.gov Subject: Undefined terms Sender: owner-qed@mcs.anl.gov Precedence: bulk I'm giving a presentation to the second QED workshop on ways of handling undefined terms (terms which should not have values or whose values we don't care about; things like 1/0 and car(nil) spring to mind). I can think of a number of approaches in the abstract; I'd like to hear what is done in actual systems. In my system, for example (at least in one theory developed under my system) 1/0 is a real number whose value we don't care about and the form of the multiplicative inverse axiom is x*(1/x) = if x = 0 then 0 else 1 Descriptions of approaches taken by different groups would be appreciated! --Randall Holmes holmes@math.idbsu.edu