deduceAlphaImplications function

DefaultMap<Logic, Set<Logic>> deduceAlphaImplications(List<(Logic, Logic)> implications)

deduce all implications

Description by example

given set of logic rules:

a -> b b -> c

we deduce all possible rules:

a -> b, c b -> c

implications: [] of (a,b) return: {} of a -> set(b, c, ...)

Implementation

DefaultMap<Logic, Set<Logic>> deduceAlphaImplications(
    List<(Logic, Logic)> implications) {
  implications += [
    for (final (i, j) in implications) (Not.create(j), Not.create(i))
  ];
  final res = DefaultMap<Logic, Set<Logic>>(() => <Logic>{});
  final fullImplications = transitiveClosure(implications);
  for (final (a, b) in fullImplications) {
    if (a == b) {
      continue; // skip a->a cyclic input
    }

    if (!res.containsKey(a)) {
      res[a] = <Logic>{};
    }
    res[a].add(b);
  }

  // clean up tautologies and check consistency
  for (final entry in res.entries) {
    final (a, impl) = (entry.key, entry.value);
    impl.remove(a);
    final na = Not.create(a);
    if (impl.contains(na)) {
      throw ArgumentError(
        "implications are inconsistent: $a -> $na $impl",
      );
    }
  }

  return res;
}