الفهرس 
IntroductionOnly 14 pages are availabe for public view
 |  | from | 84 |  |  |
| | | from | 84 | | |
Abstract
Theorem proving and compilation are very close in the sense that they both start with some given grammar to either apply it or prove it. If we are to apply it, then we are dealing with compilation. If we are attempting to prove it, then this is theorem proving. We study the theorem provers in first order logic such as VAMPIRE and tableaux methods to check a validity of a formula. The objective is to show whether a given set of formulae is satisfiable or not. If the negation of a formula is unsatisfiable then a formula is valid. We study the difference techniques of parsing such as LL(1) and SLR(1) parsing techniques, where parsing is the main stage of the compiler phases, because it is responsible for the grammatical checking of the program statement.
The dissertation comprises the following parts: (i) using some logic software that verify the theories of the first-order logic. These software are VAMPIRE and tableau software. It is worthwhile mentioning that the VAMPIRE is a fully automated method while the tableaux includes segments that must be answered manually. VAMPIRE depends on resolution and paramodulation techniques where we convert a formula to conjunctive normal form while in tableau the formula is converted to disjunctive normal form (Dual Form). (ii) Presentation of the problems of compilation including the different kinds of grammar met or dealt with in writing strings of a language. (iii) Using the JFLAP, which is a package of graphical tools in learning the basic concepts of formal languages and automata theory for compilation to verify the methodology of LL(1) and SLR(1) parsing techniques. (iv) Presenting different types of compiling such as LL(1) and SLR(1) and Computing the time consumed for each compilation method and finding the shortest of them. (v) Applying these different methods of compilation to the same strings, we conclude that SLR(1) has a shorter compilation time than LL(1).