イェール射撃問題
イェール射撃問題では、変化数が最小となるようなフルーエントへの付値(英語版)の一つは次のようなものである。
これが期待される解であり、フルーエントの変化は2回である:
l o a d e d {\displaystyle loaded} が時刻1で真になり、 a l i v e {\displaystyle alive} が時刻3で偽になる。
ところが次の付値も同じ条件を満たす。
この場合もフルーエントの変化は2回である:
l o a d e d {\displaystyle loaded} が時刻1で真になり、時刻2で偽になる。
結果的にこのような評価も状態変化の有効な記述ではあるが、しかし、時刻2で l o a d e d {\displaystyle loaded} が偽になることを説明する妥当な理由は何もない。変化の最小化という制約が「誤った」解を導き得るというこの事実が、イェール射撃問題が提案される動機となった。
イェール射撃問題は動的なシナリオの形式化に論理学を用いるにあたっての深刻な障壁だと考えられてきたが、1980年代後半から解決策が知られ始めた。その一つが、動作の特定に述語完備化(predicate completion)を用いるものである。この解決策によれば、「発砲がフレッドに死をもたらす」という事実は次の前提の下で定式化されている: a l i v e {\displaystyle alive} と l o a d e d {\displaystyle loaded} が真で、発生する帰結は a l i v e {\displaystyle alive} が真理値を変えること(つまり偽になること)であること。