Implementing Polymorphism in Zenon - Archive ouverte HAL Access content directly
Conference Papers Year : 2015

Implementing Polymorphism in Zenon

(1, 2, 3) , (2, 3, 1) , (1, 2, 3)
1
2
3

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.
Fichier principal
Vignette du fichier
zenmo.pdf (434.02 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01243593 , version 1 (15-12-2015)

Licence

Attribution - NoDerivatives - CC BY 4.0

Identifiers

  • HAL Id : hal-01243593 , version 1

Cite

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⟩
275 View
111 Download

Share

Gmail Facebook Twitter LinkedIn More