arrow
Return

Iterative Monomorphisation

delete2026-01-01
delete0
delete
OA
AI
T
Tanguy Bozec *
J
Jasmin Christian Blanchette
DOI:10.1007/978-3-032-04167-8_15delete
deleteOriginal
deleteShare
deleteSave
View PDF
Abstract

Abstract

En 中文
Monomorphisation can be used to extend monomorphic provers to support polymorphic logics. We describe a pragmatic iterative approach. We implemented it in the Zipperposition prover, where it is used to translate away polymorphism before invoking the monomorphic prover E as a backend. Our evaluation shows that this approach increases Zipperposition's success rate. Moreover, we find that iterative monomorphisation outperforms some native implementations of polymorphism.
Keywords:
Polymorphism
monomorphism
automated reasoning
AI Summary

AI Summary

Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.

Journal

F
FRONTIERS OF COMBINING SYSTEMS, FROCOS 2025
IF:
0
Papers:
21
Citations:
0

Organization

U
University of Munich
Scholars:
5.7W
Papers: 4.2W
Citations: 68
U
Universite Paris Saclay
Scholars:
7.3W
Papers: 5.3W
Citations: 540