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:
“Our argument ... will result, not upon logic by itself—though without logic we should never have got to this point—but upon the fortunate contingent fact that people who would take this logically possible view, after they had really imagined themselves in the other man’s position, are extremely rare.”
—Richard M. Hare (b. 1919)