Iterative monomorphisation

DOI10.1007/978-3-032-04167-8_15MaRDI QIDQ6852307zbMATH OpenFDO

Authors Tanguy Bozec, Jasmin Christian Blanchette

Publication date 26 February 2026

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

polymorphismautomated reasoningmonomorphism

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Logic in artificial intelligence (68T27) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• A Brief Overview of HOL4
• A Polymorphic Vampire
• Encoding monomorphic and polymorphic types
• Expressing polymorphic types in a many-sorted language
• HOL Light: An Overview
• Isabelle/HOL. A proof assistant for higher-order logic
• Lightweight relevance filtering for machine-generated resolution problems
• Making higher-order superposition work
• Optimizing proof search in model elimination
• Sine qua non for large theory reasoning
• Sledgehammer: judgement day
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0

This page was built for publication: Iterative monomorphisation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6852307)