5 found
  1.  20
    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 (7 more)  
    Export citation  
    My bibliography  
  2.  14
    Logic and Computation: Interactive Proof with Cambridge Lcf.Lawrence C. Paulson - 1987 - 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  
    My bibliography   1 citation  
  3.  3
    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.
  4.  1
    Lightweight Relevance Filtering for Machine-Generated Resolution Problems.Jia Meng & Lawrence C. Paulson - 2009 - Journal of Applied Logic 7 (1):41-57.
  5. 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.