Skip to Main content Skip to Navigation
Conference papers

Implementing Polymorphism in Zenon

Abstract : Extending first-order logic with ML-style polymorphism allows to define generic axioms dealing with several sorts. Until recently, most automated theorem provers relied on preprocess encodings into mono/many-sorted logic to reason within such theories. In this paper, we discuss the implementation of polymorphism into the first-order tableau-based automated theorem prover Zenon. This implementation led us to modify some basic parts of the code, from the representation of expressions to the proof-search algorithm.
Document type :
Conference papers
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download
Contributor : Pierre Halmagrand Connect in order to contact the contributor
Submitted on : Tuesday, December 15, 2015 - 11:02:09 AM
Last modification on : Friday, January 21, 2022 - 3:15:32 AM
Long-term archiving on: : Saturday, April 29, 2017 - 2:05:57 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License


  • HAL Id : hal-01243593, version 1



Guillaume Bury, Raphaël Cauderlier, Pierre Halmagrand. Implementing Polymorphism in Zenon. 11th International Workshop on the Implementation of Logics (IWIL), Nov 2015, Suva, Fiji. ⟨hal-01243593⟩



Les métriques sont temporairement indisponibles