Abschlussarbeit

One problem when using propositional logic is that the complexity of propositional logic depends on the number of atoms used in the logic. To reduce the number of atoms in applications, one can focus on the relevant atoms case by case. Technically, this can be done by variable forgetting (also called variable elimination), an operation defined syntactically. Given a formula 'A' defined over a signature P, the variable forgetting of an atom 'a' is the formula obtained by replacing all occurrences of 'a' in 'A' by a tautology disjointed with replacing all occurrences of 'a' in 'A' by a falsum. One can easily observe that variable forgetting is very drastic, e.g., forgetting an atom results in a tautological formula, even in cases where one might not excepted this.