My bachelor thesis. Nothing serious, formal language was not my choice!!
The Guarded Fragment is a decidable fragment of first-order logic. We are concerned with a further restriction of the Guarded Fragment, called the Forward Guarded Fragment, in which variables appear in atoms only in the order of quantification. The Guarded Fragment can be decided with the resolution method in the double exponential time. We show that the resolution method for the Guarded Fragment can be used to decide Forward Guarded Fragment in single exponential time and we provide the implementation.