Skip to content

Have the URE fully support formula premises wrapped in SetLink #16

@ngeiswei

Description

@ngeiswei

Problem

When a rule formula has a set of unordered premises they can be wrapped in a SetLink. For instance a conjunction rule can be expressed as follows

Bind
  And
    X
    Y
  ExecutionOutput
    GroundedPredicate "conjunction-formula"
    And
      X
      Y
    Set
      X
      Y

Wrapping X and Y in a SetLink allows the URE to not create multiple versions of inference trees with different permutations of X and Y. For instance without SetLink, when unifying this rule with some target And Z W it would create 2 inference trees

Bind
  And
    Z
    W
  ExecutionOutput
    GroundedPredicate "conjunction-formula"
    And
      Z
      W
    Z
    W

and

Bind
  And
    Z
    W
  ExecutionOutput
    GroundedPredicate "conjunction-formula"
    And
      Z
      W
    ;; Z and W have been swapped
    W
    Z

Motivation

Wrapping unordered formula premises in SetLink avoids over-representing semantically equivalent inference trees, which ultimately speeds up reasoning.

Task

Currently the URE only supports wrapping all formula premises in SetLink, but in some case only a subset of premises are unordered. So the task here would be to have the URE support wrapping a subset of formula premises in a SetLink.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions