tool A theorem proof system consisting of a table whose rows

contain assertions or goals. Variables in assertions are

implicitly universally quantified and variables in goals are

implicitly existentially quantified. The declarative meaning

of a tableau is that if every instance of every assertion is

true then some instance of at least one of the goals is true.