Дерево решений однократного чтения определяется следующим образом:
- и F L сек е считываются однократно деревьев решений.
- Если и B являются деревьями решений с однократным чтением, а x является переменной, не встречающейся в A и B , то ( x ∧ A ) ∨ ( ˉ x ∧ B ) также является деревом решений с однократным чтением.
Какова сложность проблемы эквивалентности для деревьев решений с однократным чтением?
- Входные данные : Два чтения один раз деревьев решений и B .
- Выход: ?
Мотивация:
Эта проблема возникла, когда я смотрел на проблему доказательной эквивалентности (перестановки правил) фрагмента линейной логики.
Ответы:
Я нашел частичное решение. Проблема в Л.
Отрицанием эквивалентна ( ° A ∧ B ) ∨ ( ∧ ˉ B ) , которая эквивалентна F L сек е тогда и только тогда как ( ··· A ∧ B ) и ( ∧ ˉ B ) есть.A↔B (A¯∧B)∨(A∧B¯) False (A¯∧B) (A∧B¯)
Так что проблема как минимум в Л.
РЕДАКТИРОВАТЬ 2: там это, http://iml.univ-mrs.fr/~bagnol/drafts/mall_bdd.pdf
Таким образом, проблема действительно завершена в Logspace.
источник
источник