| Popis: |
R-calculus is a belief revision operator satisfying AGM postulates, and belief revision in ontology engineering is ontology revision, which based logic is description logics. In Post three-valued description logic, a tableau proof system Tt will be given such that Tt is sound and complete for t-satisfiability, and nonmonotonic, that is, a theory Δ is t-satisfiable if and only if Δ is deducible in Tt. Based on the tableau proof system, an R-calculus Rt will be given such that a configuration Δ|C(a) is reducible to C(a),Δ if and only if C(a) is t-satisfiable with Δ, if and only if reduction Δ|C(a) ⇒ C(a),Δ is deducible in Rt. |
