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.
Type de document :
Communication dans un congrès
11th International Workshop on the Implementation of Logics (IWIL), Nov 2015, Suva, Fiji. 11th International Workshop on the Implementation of Logics (IWIL), 2015, 〈http://www.eprover.org/EVENTS/IWIL-2015.html〉
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01243593
Contributeur : Pierre Halmagrand <>
Soumis le : mardi 15 décembre 2015 - 11:02:09
Dernière modification le : jeudi 13 septembre 2018 - 15:24:10
Document(s) archivé(s) le : samedi 29 avril 2017 - 14:05:57

Fichier

zenmo.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

  • 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. 11th International Workshop on the Implementation of Logics (IWIL), 2015, 〈http://www.eprover.org/EVENTS/IWIL-2015.html〉. 〈hal-01243593〉

Partager

Métriques

Consultations de la notice

303

Téléchargements de fichiers

65