Theorem Proving in Higher Order Logics

DOI10.1007/11541868MaRDI QIDQ5477663zbMATH OpenOpenAlexFDO

Authors Tom Ridge, James Margetson

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 46359
• scientific article; zbMATH DE number 1926638
• scientific article; zbMATH DE number 4170865
• 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

(26)

• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• scientific article; zbMATH DE number 1761887 (Why is no real title available?)
• Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL
• A verified runtime for a verified theorem prover
• A verified SAT solver framework with learn, forget, restart, and incrementality
• scientific article; zbMATH DE number 1614710 (Why is no real title available?)
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• scientific article; zbMATH DE number 3948225 (Why is no real title available?)
• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• Programming and verifying a declarative first-order prover in Isabelle/HOL
• An extension of the Boyer-Moore theorem prover to support first-order quantification
• Formalization of the Resolution Calculus for First-Order Logic
• A naive prover for first-order logic: a minimal example of analytic completeness
• Why Would You Trust B?
• Formalization of the resolution calculus for first-order logic
• Completeness theorems for first-order logic analysed in constructive type theory
• A verified proof checker for higher-order logic
• Mechanical Verification of a Constructive Proof for FLP
• Formally verified tableau-based reasoners for a description logic
• Formalized proof systems for propositional logic
• AVATAR: The Architecture for First-Order Theorem Provers
• Soundness and completeness proofs by coinductive methods
• scientific article; zbMATH DE number 4053565 (Why is no real title available?)
• scientific article; zbMATH DE number 67454 (Why is no real title available?)
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)

Describes a project that uses

Uses Software

• Isabelle/HOL
• OCaml
• LTL2BA

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)