Verification of Generalized Inconsistency-Aware Knowledge and Action Bases (Extended Version)
This work addresses incremental improvements in formal verification for AI systems managing inconsistent knowledge, primarily relevant to researchers in knowledge representation and automated reasoning.
The paper tackles the verification of inconsistency-aware Knowledge and Action Bases by introducing Golog-KABs with a parametric execution semantics to handle various inconsistency semantics, and shows that verification of first-order temporal properties can be reduced to existing techniques for standard KABs.
Knowledge and Action Bases (KABs) have been put forward as a semantically rich representation of a domain, using a DL KB to account for its static aspects, and actions to evolve its extensional part over time, possibly introducing new objects. Recently, KABs have been extended to manage inconsistency, with ad-hoc verification techniques geared towards specific semantics. This work provides a twofold contribution along this line of research. On the one hand, we enrich KABs with a high-level, compact action language inspired by Golog, obtaining so called Golog-KABs (GKABs). On the other hand, we introduce a parametric execution semantics for GKABs, so as to elegantly accomodate a plethora of inconsistency-aware semantics based on the notion of repair. We then provide several reductions for the verification of sophisticated first-order temporal properties over inconsistency-aware GKABs, and show that it can be addressed using known techniques, developed for standard KABs.