Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMath1152.03314OpenAlexW2484880499MaRDI QIDQ5477651

Peter V. Homeier

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)

Related Items

Quotients of Bounded Natural Functors, Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, Quotients by Idempotent Functions in Cedille, Combining higher-order logic with set theory formalizations, Unnamed Item, Unnamed Item, Nominal techniques in Isabelle/HOL, Higher-Order Tarski Grothendieck as a Foundation for Formal Proof., General Bindings and Alpha-Equivalence in Nominal Isabelle

Uses Software

• Isabelle/HOL
• PVS