Consistency Checks

To preempt inconsistent belief change scenarios, COBA 2.0 prohibits certain kinds of input formulas that result in inconsistent belief change scenarios. Automatic consistency checks on input formulas, although carried out by default, can be optionally disabled by users wishing to speed up computations. One caveat is that, if these checks are disabled, F might be obtained as the resulting knowledge base.

Let $(\bigwedge Rev)$ denote the conjunction of all formulas in $Rev$ for revision, $(\bigwedge EB IC)$ the conjunction of all entailment-based integrity constraints. You should avoid he following inconsistent belief change scenarios; sample error messages, where applicable, are italicized.

1. a contradiction in $Rev$:
   The conjunction of revisions is inconsistent!

2. a contradiction in $EB IC$:
   The conjunction of EB ICs is a contradiction!

3. a contradiction as a KB, revision, or EB IC formula: No error message; sentence not added.

4. a tautolgy as a contraction formula:
   No error message; sentence not added.

5. a contradiction as a CB IC formula:
   No error message; sentence not added.

6. conflict between $(\bigwedge Rev)$ and $(\bigwedge EB IC)$:
   The conjunction of revisions is inconsistent with the conjunction of EB ICs!

7. conflict between $(\bigwedge Rev)$ and contraction formulas:
   The contraction indexed 0 is inconsistent with the conjunction of revisions (indexing starts at 0)!

8. conflict between $(\bigwedge Rev)$ and CB IC formulas:
   The CB IC indexed 1 is inconsistent with the conjunction of revisions (indexing starts at 0)!

9. conflict between $(\bigwedge EB IC)$ and contraction formulas:
   The contraction indexed 6 is inconsistent with the conjunction of EB ICs (indexing starts at 0)!

10. conflict between $(\bigwedge EB IC)$ and CB IC formulas:
    The CB IC indexed 3 is inconsistent with the conjunction of EB ICs (indexing starts at 0)!

11. conflicting pairs of CB IC formulas and contraction formulas:
    The contraction indexed 2 is inconsistent with the CB IC indexed 0 (indexing starts at 0)!