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
Liste complète des métadonnées

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/hal-01243593
Contributor : Pierre Halmagrand <>
Submitted on : Tuesday, December 15, 2015 - 11:02:09 AM
Last modification on : Saturday, February 9, 2019 - 1:25:17 AM
Document(s) archivé(s) le : Saturday, April 29, 2017 - 2:05:57 PM

File

zenmo.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License

Identifiers

  • HAL Id : hal-01243593, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

392

Files downloads

151