Typically it is considered a strength of a language that the same situation can be described in different ways. However, when a human or a program is to check whether two representations are essentially the same it is much easier to deal with normal forms. For instance, (infinitely many) different sets of formulae may normalize to the same clause set. In the case of propositional logic formulae with a fixed number of boolean variables, the class of all clause sets is finite. Since it grows doubly exponentially, it is not feasible to construct the complete class even for small numbers of boolean variables. Hence further normalizations are necessary and will be studied. Furthermore some potential applications will be discussed.
|Number of pages||10|
|Journal||Lecture Notes in Computer Science|
|Publication status||Published - 1 Jan 2008|
|Event||Intelligent Computer Mathematics: Joint Proceedings of AISC 2008, Calculemus 2008 and MKM 2008 - Birmingham, United Kingdom|
Duration: 28 Jul 2008 → 1 Aug 2008