Normal forms of conditional knowledge bases respecting system P-entailments and signature renamings (Q2075376): Difference between revisions

The paper revises and extends the work presented in [the authors, Lect. Notes Comput. Sci. 12012, 22--41 (2020; Zbl 1456.68184)]. The setting is that of conditional logic, built upon a finite set \(\Sigma\) of propositional letters, with formulas (conditionals) of the form \((B|A)\) with \(A\) and \(B\) propositional formulas over \(\Sigma\) meant to express that \textit{if \(A\) then usually \(B\)}; for instance, \((e\overline{f}|e)\) can formalise that ``e-cars usually are e-cars that do not need fossil fuel''. The semantics is defined on the basis of \textit{ordinal conditional functions} (OCF), that map possible worlds to plausibilities, in the form of natural numbers, lower numbers corresponding to ``less surprise''. An OCF \(\kappa\) then accepts a conditional \((B|A)\), written \(\kappa\models (B|A)\) if \(\kappa(AB)<\kappa(A\overline{B})\) (verification of the conditional is less surprising than its falsification). Given a knowledge base \(\mathcal R\), all models of \(\mathcal R\) accept a conditional \((B|A)\) iff \((B|A)\) can be derived from \(\mathcal R\) using the 6 rules of system P [\textit{D. Lehmann} and \textit{M. Magidor}, Artif. Intell. 55, No. 1, 1--60 (1992; Zbl 0762.68057)]. The paper proposes: \begin{itemize} \item a notion of unique renaming normal form (\(\rho\)NF) for knowledge bases thanks to which signatures can be renamed; \item a reduced antecedent normal form (RANF) for knowledge bases, taking system P inferences into account; \item a renaming antecedent normal form (\(\rho\)ANF) and a renaming reduced antecedent normal form (\(\rho\)RANF) that combine \(\rho\)NF with ANF and RANF, respectively; \item algorithms for transforming a knowledge base into any of the introduced normal forms; \item an algorithm to systematically generate all knowledge bases in \(\rho\)RANF normal form over a given signature that are consistent, pairwise not antecedentwise equivalent and pairwise not equivalent under signature renaming. \end{itemize}