24 citations · 40 across the 18 of their papers we have counts for
5 papers · 1 filter
Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
Mnacho Echenim, Hervé Guiol, Nicolas Peltier
We formalize in the proof assistant Isabelle essential basic notions and results in financial mathematics. We provide generic formal definitions of concepts such as markets, portfo…
A Generic Framework for Implicate Generation Modulo Theories
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
The clausal logical consequences of a formula are called its implicates. The generation of these implicates has several applications, such as the identification of missing hypothes…
The Complexity of Prenex Separation Logic with One Selector
Mnacho Echenim, Radu Iosif, Nicolas Peltier
We first show that infinite satisfiability can be reduced to finite satisfiability for all prenex formulas of Separation Logic with selector fields ($\seplogk{k}$). Second…
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
Mnacho Echenim, Radu Iosif, Nicolas Peltier
This paper investigates the satisfiability problem for Separation Logic, with unrestricted nesting of separating conjunctions and implications, for prenex formulae with quantifier…
A Tableaux Calculus for Reducing Proof Size
Michael Peter Lettmann, Nicolas Peltier
A tableau calculus is proposed, based on a compressed representation of clauses, where literals sharing a similar shape may be merged. The inferences applied on these literals are…