During the last years, the activities of knowledge formalization and sharing useful to allow for semantically enabled management of information have been attracting growing attention, expecially in distributed environments like the Web. In this report, after a general introduction about the basis of knowledge abstraction and its formalization through ontologies, we briefly present a list of relevant formal languages used to represent knowledge: CycL, FLogic, LOOM, KIF, Ontolingua, RDF(S) and OWL. Then we focus our attention on the Web Ontology Language (OWL) and the Knowledge Interchange Format (KIF). OWL is the main language used to describe and share ontologies over the Web: there are three OWL sublanguages with a growing degree of expressiveness. We describe its structure as well as the way it is used in order to reasons over asserted knowledge. Moreover we briefly present three relevant OWL ontology editors: Prot´eg´e, SWOOP and Ontotrack and two important OWL reasoners: Pellet and FACT++. KIF is mainly a standard to describe knowledge among different computer systems so as to facilitate its exchange. We describe the main elements of KIF syntax; we also consider Sigma, an environment for creating, testing, modifying, and performing inference with KIF ontologies. We comment some meaningful example of both OWL and KIF ontologies and, in conclusion, we compare their main expresive features.