First-order Logic Tableau
Tableaux are extended to first order predicate logic by two rules for dealing with universal and existential quantifiers, respectively. Two different sets of rules can be used; both employ a form of Skolemization for handing existential quantifiers, but differ on the handling of universal quantifiers.
The set of formulae to check for validity is here supposed to contain no free variables; this is not a limitation as free variables are implicitly universally quantified, so universal quantifiers over these variables can be added, resulting in a formula with no free variables.
Read more about this topic: Method Of Analytic Tableaux
Famous quotes containing the word logic:
“...some sort of false logic has crept into our schools, for the people whom I have seen doing housework or cooking know nothing of botany or chemistry, and the people who know botany and chemistry do not cook or sweep. The conclusion seems to be, if one knows chemistry she must not cook or do housework.”
—Ellen Henrietta Swallow Richards (1842–1911)