8 found
Order:
  1.  31
    The Higher-Order Prover LEO-II.Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson & Frank Theiß - 2015 - Journal of Automated Reasoning 55 (4):389-404.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   8 citations  
  2. Quantified Multimodal Logics in Simple Type Theory.Christoph Benzmüller & Lawrence C. Paulson - 2013 - Logica Universalis 7 (1):7-20.
    We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  3.  20
    A formalised theorem in the partition calculus.Lawrence C. Paulson - 2024 - Annals of Pure and Applied Logic 175 (1):103246.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  4.  29
    A machine-assisted proof of gödel’s incompleteness theorems for the theory of hereditarily finite sets.Lawrence C. Paulson - 2014 - Review of Symbolic Logic 7 (3):484-498.
  5.  30
    Logic and computation: interactive proof with Cambridge LCF.Lawrence C. Paulson - 1987 - New York: Cambridge University Press.
    Logic and Computation is concerned with techniques for formal theorem-proving, with particular reference to Cambridge LCF (Logic for Computable Functions). Cambridge LCF is a computer program for reasoning about computation. It combines methods of mathematical logic with domain theory, the basis of the denotational approach to specifying the meaning of statements in a programming language. This book consists of two parts. Part I outlines the mathematical preliminaries: elementary logic and domain theory. They are explained at an intuitive level, giving references (...)
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  6.  46
    Ackermann’s function in iterative form: A proof assistant experiment.Lawrence C. Paulson - 2021 - Bulletin of Symbolic Logic 27 (4):426-435.
    Ackermann’s function can be expressed using an iterative algorithm, which essentially takes the form of a term rewriting system. Although the termination of this algorithm is far from obvious, its equivalence to the traditional recursive formulation—and therefore its totality—has a simple proof in Isabelle/HOL. This is a small example of formalising mathematics using a proof assistant, with a focus on the treatment of difficult recursions.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  7.  37
    Lightweight relevance filtering for machine-generated resolution problems.Jia Meng & Lawrence C. Paulson - 2009 - Journal of Applied Logic 7 (1):41-57.
  8.  22
    LEO-II and Satallax on the Sledgehammer test bench.Nik Sultana, Jasmin Christian Blanchette & Lawrence C. Paulson - 2013 - Journal of Applied Logic 11 (1):91-102.