In order to model context in pervasive computing environments, and support logic-based context reasoning, a core ontology modeling framework for OWL-S(Ontology Web Language for Services) and a reasoning mechanism using F-logic are proposed in this paper. It analyzes the construction of OWLS model type, gives F-logic axioms, derivation rules and methods to check the consistency and satisfiability of context information. The mechanism and method can verify some global attributes of Semantic Web system by model checking based on first-order logic, provide formal model for OWL-S, and expand its expression ability and verification ability.