명제 논리

Question

다음과 같은 문제가 있습니다 :

나는 두 개의 명제식이 논리적으로 동일해야합니다. 오직 그 중 하나는 변수가 어떤 명제식으로 대체 될 수 있다는 의미에서 '변수'를 포함합니다. 이제 문제는 논리 대체가 사실이되도록 변수의 실제 대체 값을 찾아야한다는 것입니다. 예 :

(a^~ b)는 x = 여기

는, x는 변수이다. 이 동치는^B와 X를 대체함으로써, 진정한 이루어질 수 있으므로된다 :

(a^~ b) 또는 (A^B) 그래서이 문제이다

를 =. 나는 입력으로 "하나의 변수 x를 가진 방정식"을 얻고 방정식이 논리적 인 동등성이되도록 변수 x에 대한 출력 값을 제공하는 알고리즘이 필요합니다.

항상 하나의 변수가 있습니다. (실제로 하나 이상의 변수에 문제가 발생할 수 있지만 먼저 간단한 경우를 해결하고 싶습니다.) 문제의 수식은 CNF 또는 DNF에없는 형식을 가질 수 있습니다. 또한 수식은 실제로 FALSE 또는 TRUE 일 수 있으며 솔루션이없는 경우가 있습니다 (예 : "a 또는 x = false", 솔루션이 없음) 또는 둘 이상의 솔루션 (예 : "a 및 x = false "잘못된 제안은 유효한 대답이 될 것입니다.)

나는 공식이 만족 스러운지 아닌지를 알려주는 tableaux reasoner입니다. 그래서 시험을 테스트 할 수 있습니다. 하지만 제 문제는 저에게 해결책을 제시하는 것입니다.

Answer 1

나는 당신이 찾고있는 것이 해석되지 않은 기능을 처리 할 수있는 추론 엔진이라고 믿습니다. 이러한 엔진은 기능을 포함하는 문제를 처리 할 수 ​​있습니다 예를 들어,

(A^~ B) 또는 F 그들은 실제로 생성,의 (a는 b)는

을 = 그들은 일반적으로 즉, 모델을 생산할 수 있습니다 초기 공식을 만족하는 함수 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은 유한 도메인 (예 : 부울)에 대한 수량 한정자에 대해 완전한 추론 엔진을 사용하고 그러한 수식에 대한 모델을 생성 할 수 있습니다.