RACER is a reasoner for the description logic SHIQ, implementing a TBox and ABox reasoner. It was the first full-fledged ABox description logic system for a very expressive logic, based on optimized sound and complete algorithms. RACER also implements a decision procedure for modal logic satisfiability problems. SHIQ extends ALCNH_R+ by adding qualified number restrictions and inverse roles. ALCQHI_R+ is a variant of SHIQ. The logic includes concept names, role names, and individual names. Roles are divided into non-transitive and transitive. Number restrictions are only allowed for simple roles. Inverse roles can be used instead of role names. A concept is consistent if it has a model that satisfies the TBox. An ABox is consistent if it has a model that satisfies the TBox. A knowledge base is consistent if there exists a model that satisfies both the TBox and ABox. Inference services include subsumption, consistency checking, and instance checking. RACER supports multiple TBoxes and ABoxes, allowing assertions to be added after queries. It provides various inference services, including concept ancestors, direct types, and role fillers. The system uses tableaux calculus for ABox consistency and integrates optimization techniques like dependency-directed backtracking and DPLL-style semantic branching. RACER's architecture is inspired by optimization techniques for TBox reasoning, including axiom transformations, model caching, and merging. It is implemented in Common Lisp and available as a server program for research purposes. It supports interfaces for Java, Common Lisp, and C/C++. RACER has been applied in ontology engineering, telecommunication systems, and database integration. Future work includes integrating techniques for concrete domains and optimizing number restrictions.RACER is a reasoner for the description logic SHIQ, implementing a TBox and ABox reasoner. It was the first full-fledged ABox description logic system for a very expressive logic, based on optimized sound and complete algorithms. RACER also implements a decision procedure for modal logic satisfiability problems. SHIQ extends ALCNH_R+ by adding qualified number restrictions and inverse roles. ALCQHI_R+ is a variant of SHIQ. The logic includes concept names, role names, and individual names. Roles are divided into non-transitive and transitive. Number restrictions are only allowed for simple roles. Inverse roles can be used instead of role names. A concept is consistent if it has a model that satisfies the TBox. An ABox is consistent if it has a model that satisfies the TBox. A knowledge base is consistent if there exists a model that satisfies both the TBox and ABox. Inference services include subsumption, consistency checking, and instance checking. RACER supports multiple TBoxes and ABoxes, allowing assertions to be added after queries. It provides various inference services, including concept ancestors, direct types, and role fillers. The system uses tableaux calculus for ABox consistency and integrates optimization techniques like dependency-directed backtracking and DPLL-style semantic branching. RACER's architecture is inspired by optimization techniques for TBox reasoning, including axiom transformations, model caching, and merging. It is implemented in Common Lisp and available as a server program for research purposes. It supports interfaces for Java, Common Lisp, and C/C++. RACER has been applied in ontology engineering, telecommunication systems, and database integration. Future work includes integrating techniques for concrete domains and optimizing number restrictions.