Theorem Proving in Higher Order Logics
From MaRDI portal
Publication:5477663
DOI10.1007/11541868zbMATH Open1152.03316OpenAlexW2484880499MaRDI QIDQ5477663FDOQ5477663
Publication date: 6 July 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11541868
Recommendations
- scientific article
- scientific article; zbMATH DE number 1926638
- scientific article
- scientific article; zbMATH DE number 7699423
- A verified proof checker for higher-order logic
- scientific article; zbMATH DE number 1300967
- A theorem prover for a computational logic
- Publication:3490989
- scientific article; zbMATH DE number 1070624
- First-order theorem proving: foreword
Cited In (25)
- An extension of the Boyer-Moore theorem prover to support first-order quantification
- Title not available (Why is that?)
- Title not available (Why is that?)
- AVATAR: The Architecture for First-Order Theorem Provers
- Mechanical Verification of a Constructive Proof for FLP
- Formalization of the resolution calculus for first-order logic
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Title not available (Why is that?)
- Title not available (Why is that?)
- A verified proof checker for higher-order logic
- Why Would You Trust B?
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL
- Soundness and completeness proofs by coinductive methods
- Formalization of the Resolution Calculus for First-Order Logic
- Title not available (Why is that?)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- Title not available (Why is that?)
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Formally verified tableau-based reasoners for a description logic
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- Title not available (Why is that?)
- A naive prover for first-order logic: a minimal example of analytic completeness
- A Verified Runtime for a Verified Theorem Prover
- Title not available (Why is that?)
Uses Software
This page was built for publication: Theorem Proving in Higher Order Logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5477663)
