That's very good project, Ahmed. First thing you need to make sure what the tweet really means. That's the most difficult task. Once you know exactly what it means then it would be rather straightforward to put it in symbolic form.

But finding out what some tweets mean is beyond the capability of any algorithm I think. Because to know the actual meanings in many cases you have to rely on contexts, but algorithm does not always have a means to know that. Maybe before you input the tweets to the machine you would nee to supply the context and so on. In short you have to interpret the tweet first and then let the machine do the translation.

Thanks for the cool response, Dr. Hongladarom! The idea of relying on a context is indeed in mind. For example, understanding the sentiments of electronic cigarette comes to mind is a good application. Perhaps staring with a finite set of vocabularies and analyzing their corresponding tweets in pure symbolic logic manner is a good start. Please feel free to share any other thoughts that may cross your mind. I very much appreciate it!

It sort of depends on what you mean by translate. In the naive sense, of translating sentences into propositional calculus, I have my doubts because natural language is not very malleable to be translated into logic, even if it is grammatical language. On the other hand there is a vibrant Natural Language Processing community that has tools to extract the existence of named entities, noun phrases and some of the ways these are qualified. Of course the result of such an analysis is already a formal statement but I don't think it is usually written that way. There is no lack of tools: have a look at the Pattern/CLIPS (www.clips.ua.ac.be/pattern), and  the NLTK (www.nltk.org/) libraries (both Python) , tools around Gate (https://gate.ac.uk/) or tools on this site:  http://opennlp.sourceforge.net/projects.html  (mostly Java) For context, try open Calais from Reuters. 

Have you considered looking at Hashtags?  They can help with meaning and can be useful if in future you intend on trying to analyse data in terms of your project.  Best of luck!

@Marjorie Newson. In theory hashtags are like keywords, in practice people use them creatively as a twitter specific "literary" style, often making the true intentions of the writer clear.

@MarjorieNewson I did much with Hashtags, my PhD dissertation was about K-H networks, constructed from keywords and hashtags. I still need this step as preliminary step for the networks though

@DrRogierBrussee Hashtags are more complex because they can be about a simple, number, or a set of words. This actually requires another algorithm to make associate semantics with the hashtag. This is actually on the menu by using means of word segmentation algorithm of a sort. Thanks for all responses. I am delighted!

This remembers me of a nice cartoon in a comic book. An inventor is very proud to have invented the headphone able to translate what do the animals say. He goes away to check his invention. He sees a dog barking: waw! waw! ... waw!...  waw! waw! Now he puts his headphones and hears the following: Hey! Hey! ... Hey you!...  Hey! Hey! There was no more meaning in the dog's language, thing which could have been thought before...

The "moral", if any, is that one can do such a formalization only over the meaning of tweets. The only one possibility to start with is to do a list of short-cuts and abbreviations used in  tweeting. Then a graph about how such abbreviations connect logically together, Last but not least, to study to what extent some tweet message differ from the normal list of abbreviations. The last part is the most difficult, and is also the reason why we do not speak about one project of research, but about complex multidisciplinary study over a many years ...

The first step could be building normalized syntactic constructs using one of the many semantic parsers that exploit the gigantic web data bases to "interpret" texts.

Then it should be easy to translate the outcome into predicates to be run by a logical engine, e.g Prolog. 

 I believe that the most significant task is identifying the predicates (both unary and binary) with regard to the meaning of the tweet.