RACER System Description

RACER System Description

| Volker Haarslev and Ralf Möller
RACER is a system that implements a TBox and ABox reasoner for the logic SHIQ, which extends the logic $\mathcal{ALCN}\mathcal{H}_R$ by adding qualified number restrictions and inverse roles. It is the first full-fledged ABox description logic system for an expressive logic and is based on optimized sound and complete algorithms. RACER also provides a decision procedure for modal logic satisfiability problems, possibly with global axioms. The introduction explains the syntax and semantics of $\mathcal{ALCQH}_R$, a description logic that includes concept names, role names, and individual names. It defines role hierarchies, sub-roles, and terminological axioms (TBoxes). The system supports various inference services, such as computing subsumption relationships, checking consistency, and retrieving instances and roles. The architecture of RACER incorporates optimization techniques like dependency-directed backtracking and DPLL-style semantic branching to ensure efficient performance. It supports multiple TBoxes and ABoxes, allowing assertions to be added or retracted after queries. RACER is implemented in Common Lisp and is available as a server program for research purposes. Applications of RACER include ontology engineering, telecommunication systems, solving modal logic satisfiability problems, and database integration tasks. Future developments will focus on integrating techniques for representing concrete domains and optimizing handling of qualified number restrictions.RACER is a system that implements a TBox and ABox reasoner for the logic SHIQ, which extends the logic $\mathcal{ALCN}\mathcal{H}_R$ by adding qualified number restrictions and inverse roles. It is the first full-fledged ABox description logic system for an expressive logic and is based on optimized sound and complete algorithms. RACER also provides a decision procedure for modal logic satisfiability problems, possibly with global axioms. The introduction explains the syntax and semantics of $\mathcal{ALCQH}_R$, a description logic that includes concept names, role names, and individual names. It defines role hierarchies, sub-roles, and terminological axioms (TBoxes). The system supports various inference services, such as computing subsumption relationships, checking consistency, and retrieving instances and roles. The architecture of RACER incorporates optimization techniques like dependency-directed backtracking and DPLL-style semantic branching to ensure efficient performance. It supports multiple TBoxes and ABoxes, allowing assertions to be added or retracted after queries. RACER is implemented in Common Lisp and is available as a server program for research purposes. Applications of RACER include ontology engineering, telecommunication systems, solving modal logic satisfiability problems, and database integration tasks. Future developments will focus on integrating techniques for representing concrete domains and optimizing handling of qualified number restrictions.
Reach us at info@study.space