A Formally Verified Prover for the $\mathcal{ALC\,}$ Description Logic

DOI10.1007/978-3-540-74591-4_11zbMath1144.68350OpenAlexW1929438219MaRDI QIDQ3523171

Francisco Jesús Martín-Mateos, María José Hidalgo, José Luis Ruiz-Reina, Joaquín Borrego-Díaz, Jose Antonio Alonso

Publication date: 2 September 2008

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

Full work available at URL: https://doi.org/10.1007/978-3-540-74591-4_11

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Related Items (4)

Verified Decision Procedures for Modal Logics. ⋮ Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations ⋮ Axiomatic and dual systems for constructive necessity, a formally verified equivalence ⋮ Formally verified tableau-based reasoners for a description logic

Uses Software

• PVS
• FaCT++

This page was built for publication: A Formally Verified Prover for the $\mathcal{ALC\,}$ Description Logic