The Logic of Choice

The choice construct (choose x : '(x)) is useful in software speci cations. We study extensions of rst-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. Part I

• Type: Journal
• Year: 2000
• Where: JSYML
• Authors: Andreas Blass, Yuri Gurevich
• Keywords: JSYML 2000, Rst-order Logic, Software Speci Cations, Useful