Automated Reasoning in $\mathcal{ALCQ}$ via SMT

DOI10.1007/978-3-642-22438-6_22zbMath1341.68226OpenAlexW160292340MaRDI QIDQ5200031

Roberto Sebastiani, Volker Haarslev, Michele Vescovi

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_22

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Knowledge representation (68T30)

Related Items (2)

Deciding Extended Modal Logics by Combining State Space Generation and SAT Solving ⋮ Automated Reasoning in $\mathcal{ALCQ}$ via SMT

Uses Software

• Pellet
• MathSAT
• FaCT++
• Racer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic tableau reasoning for the description logic \(\mathcal{SHOQ}\)
• Satisfiability Modulo the Theory of Costs: Foundations and Applications
• Practical reasoning with qualified number restrictions: A hybrid Abox calculus for the description logic 𝒮ℋ𝒬
• Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability
• Practical reasoning for very expressive description logics
• Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis
• Automated Reasoning in $\mathcal{ALCQ}$ via SMT

This page was built for publication: Automated Reasoning in $\mathcal{ALCQ}$ via SMT