Шаблонное соответствие с ассоциативными и коммутативными операторами

Шаблонное сопоставление (как, например, в Prolog, языках семейства ML и различных оболочках экспертных систем) обычно работает путем сопоставления запроса с данными элемент за элементом в строгом порядке.

Однако в таких областях, как автоматическое доказательство теорем, необходимо учитывать, что некоторые операторы являются ассоциативными и коммутативными. Предположим, у нас есть данные

A or B or C

и запрос

C or $X

По поверхностному синтаксису это не совпадает, но логически это должно совпадать с $X, связанным с A или B, потому что или ассоциативны и коммутативны.

Есть ли какая-нибудь существующая система, на любом языке, которая делает подобные вещи?