The Logic of Choice

Abstract
The choice construct (choosex: φ(x)) is useful in software specifications. We study extensions of first-order logic with the choice construct. We prove some results about Hilbert'sεoperator, but in the main part of the paper we consider the case when all choices are independent.

This publication has 8 references indexed in Scilit: