Theorem Proving in Higher Order Logics
From MaRDI portal
Publication:5477663
DOI10.1007/11541868zbMath1152.03316OpenAlexW2484880499MaRDI QIDQ5477663
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
Related Items (13)
Soundness and completeness proofs by coinductive methods ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ Formalization of the resolution calculus for first-order logic ⋮ Why Would You Trust B? ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Programming and verifying a declarative first-order prover in Isabelle/HOL ⋮ A verified proof checker for higher-order logic ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ A Verified Runtime for a Verified Theorem Prover ⋮ Formalization of the Resolution Calculus for First-Order Logic ⋮ Formally verified tableau-based reasoners for a description logic
Uses Software
This page was built for publication: Theorem Proving in Higher Order Logics
