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; Thu, 21 Sep 1995 05:19:40 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA061374820; Wed, 20 Sep 1995 21:40:20 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from tuminfo2.informatik.tu-muenchen.de by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA061344807; Wed, 20 Sep 1995 21:40:07 -0600 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <26474-3>; Thu, 21 Sep 1995 05:04:14 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8083>; Thu, 21 Sep 1995 05:04:05 +0200 From: Konrad Slind To: info-hol@leopard.cs.byu.edu, isabelle-users@cl.cam.ac.uk, christine.paulin@lip.ens-lyon.fr, cristina.cornes@inria.fr Subject: Paper available: "Function Definition in Higher-Order Logic" Message-Id: <95Sep21.050405met_dst.8083@sunbroy14.informatik.tu-muenchen.de> Date: Thu, 21 Sep 1995 05:03:51 +0200 A paper about a mechanization of the wellfounded recursion theorem is available by anonymous ftp at ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/slind/papers/wfrec.ps.Z ABSTRACT: We use a formally proven wellfounded recursion theorem as the basis upon which to build a function definition facility for Higher Order Logic. This approach offers flexibility in the choice of wellfounded relations used, the deferral of termination arguments, and automatic isolation of termination conditions. Building on this platform, we provide the ability to define recursive functions via pattern matching. The system is parameterized and has already been instantiated to quite different theorem provers (HOL and Isabelle). All comments are welcome. Konrad.