Логика высказываний - PullRequest
Новая
       29

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

1 голос
/ 16 сентября 2011

У меня есть следующая проблема:

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

(a ^ ~ b) или x = a

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

(a ^ ~ b) или (a ^ b) = a

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

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

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

1 Ответ

1 голос
/ 13 октября 2011

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

(a ^ ~ b) или f (a, b) = a

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

...