Логика высказываний

У меня такая проблема:

У меня есть две пропозициональные формулы, которые должны стать логически эквивалентными. Только один из них содержит «переменную» в том смысле, что переменную можно заменить любой пропозициональной формулой. Теперь проблема в том, что мне нужно найти фактическую замену переменной, чтобы логическая эквивалентность стала истинной. Пример:

(a ^ ~b) or x = a

Здесь x обозначает переменную. Эту логическую эквивалентность можно сделать истинной, заменив x на a ^ b, так что получится:

(a ^ ~b) or (a ^ b) = a

Так вот в чем проблема. Мне нужен алгоритм, который получает на входе «уравнение с одной переменной x» и дает на выходе значение для переменной x, так что уравнение становится логической эквивалентностью.

Всегда будет одна переменная. (на самом деле у меня могут возникнуть проблемы с более чем одной переменной, но сначала я хочу решить простой случай). Причем рассматриваемые формулы могут иметь любую форму (их нет в CNF или DNF). Кроме того, формулы могут быть ЛОЖЬ или ИСТИНА, и бывают случаи, когда нет решения (например, для «a или x = false» нет решения) или более одного решения (например, для «a и x = false» "любое ложное предложение было бы правильным ответом).

Все, что у меня есть, - это составитель таблиц, который говорит мне, выполнима ли формула или нет. Итак, я могу протестировать решение. Но моя проблема в том, чтобы просто дать мне решение.


logic satisfiability
person TRX    schedule 16.09.2011    source источник
comment
Нет, я реализую алгоритм поиска доказательств для очень специфической логики. По сути, это превращает проблему в логику высказываний, и это одна из проблем, с которой я сталкиваюсь.   -  person TRX    schedule 16.09.2011

Ответы (1)


arrow_upward
1
arrow_downward

Я считаю, что вам нужен механизм рассуждений, который может обрабатывать неинтерпретируемые функции. Такие движки могут обрабатывать проблемы, которые содержат функции, например,

(a ^ ~b) or f(a,b) = a

и они обычно могут создавать модели, т.е. они фактически генерируют функцию f (...), которая удовлетворяет вашей исходной формуле. Одним из примеров подходящих механизмов рассуждений являются так называемые решатели SMT (см. SMT-LIB). Популярным решателем является Z3 от Microsoft (см. Z3).

Пример можно представить в формате SMT-LIB следующим образом:

(set-option :produce-models true)
(declare-const a Bool)
(declare-const b Bool)
(declare-fun f (Bool Bool) Bool)

(assert (= (or (xor a (not b)) (f a b)) a))
(check-sat)
(get-model)
(exit)

и Z3 производит модель

(define-fun f ((x!1 Bool) (x!2 Bool)) Bool 
  (ite (and (= x!1 false) (= x!2 true)) false false))

что удовлетворяет исходной задаче. В общем, решение только удовлетворяет проблему. Для получения полных решений можно использовать кванторы. Не все решатели SMT поддерживают их, но Z3, например, использует полный механизм рассуждений для кванторов в конечных областях (таких как логические значения) и может создавать модели для таких формул.

person Christoph Wintersteiger    schedule 12.10.2011