Item request has been placed! ×
Item request cannot be made. ×
loading  Processing Request

Running a Prover in a Prover - Isabelle as a Meta-Logic

Item request has been placed! ×
Item request cannot be made. ×
loading   Processing Request
Read More Add to Saved list
  • Author(s): Villadsen, Jørgen
  • Source:
    Villadsen , J 2016 , ' Running a Prover in a Prover - Isabelle as a Meta-Logic ' , CADILLAC Workshop , Copenhagen , Denmark , 23/05/2016 - 25/05/2016 .
  • Document Type:
    conference object
  • Language:
    English
  • Additional Information
    • Publication Date:
      2016
    • Collection:
      Technical University of Denmark: DTU Orbit / Danmarks Tekniske Universitet
    • Abstract:
      Isabelle provides a foundation of mathematics and I show how you can run your own verified prover directly in the Isabelle prover or as a stand-alone program. I describe the formalization of syntax and semantics and discuss the proof of soundness and completeness for a simple prover for first-order logic.
    • File Description:
      application/pdf
    • Online Access:
      https://orbit.dtu.dk/en/publications/89dc3d39-f910-4467-950d-d918dc7fccc9
      https://backend.orbit.dtu.dk/ws/files/128004646/Villadsen.pdf
    • Rights:
      info:eu-repo/semantics/openAccess
    • Accession Number:
      edsbas.BD6FDDE7