Bernie-Schonfinkel의 공식은 정확히 무엇입니까?

Question

나는 간단한 명제가있다. 엄격하게 정렬 된 정수 목록의 첫 번째 요소는 목록의 모든 요소 중 최소값이라고 주장하고 싶습니다. 정렬 된 목록을 정의하는 방법은 모든 요소가 다음 요소보다 작다는 로컬 불변 식을 정의하는 것입니다. 나는 Z3에 다음과 같은 방법으로 내 제안을 공식화 한 -

---

(set-option :mbqi true) 
(set-option :model-compact true) 

(declare-fun S (Int) Bool) 
(declare-fun preceeds (Int Int) Bool) 
(declare-fun occurs-before (Int Int) Bool) 

;; preceeds is anti-reflexive 
(assert (forall ((x Int)) (=> (S x) (not (preceeds x x))))) 

;; preceeds is monotonic 
(assert (forall ((x Int) (y Int)) (=> (and (S x) (and (S y) (and (preceeds x y)))) 
             (not (preceeds y x))))) 
;; preceeds is a function 
(assert (forall ((x Int) (y Int) (z Int)) (=> (and (S x) (and (S y) (and (S z) (and (preceeds x y) 
              (preceeds x z))))) 
              (= y z)))) 
;; preceeds induces local order 
(assert (forall ((x Int) (y Int)) (=> (and (S x) (and (S y) (preceeds x y))) 
             (< x y)))) 

;; preceeds implies occurs-before 
(assert (forall ((x Int) (y Int)) (=> (and (and (S x) (S y)) (preceeds x y)) 
              (occurs-before x y)))) 

;;occurs-before is transitivie 
(assert (forall ((x Int)(y Int)(z Int)) 
    (=> (and (S x) (and (S y) (and (S z)(and (occurs-before x y) (occurs-before y z))))) 
    (occurs-before x z)) 
))    

(declare-const h Int) 
(assert (S h)) 
(assert (forall ((x Int)) (=> (S x) (occurs-before h x)))) 
(assert (forall ((y Int)) (=> (S y) (< h y)))) 
(check-sat) 
(get-model)                

---

첫째, 나는 효과적으로 명제이다 식의 어떤 클래스 정확히 알고 싶습니다. 내 주장을 효과적으로 명제로 분류 할 수 있습니까? 두 번째로 위에 제시된 제형이 맞습니까? 셋째, 효과적으로 명제가있는 경우에만 수량화 된 수식을 수락하기 위해 Z3에서 어떤 옵션을 설정해야합니까?

Answer 1

수식은 술어, 상수, 범용 한정 기호 만 포함하고 이론 (예 : 산술)을 사용하지 않으면 효과적으로 명제 단편에 있습니다. 수식에 Exists* Forall* 수량 한정자 접두사가 있고 조건 자만 사용한다는 대체 정의를 찾는 것은 매우 일반적입니다. 실존 적 수량 화기는 새로운 해석되지 않은 상수를 사용하여 제거 될 수 있으므로 이러한 정의는 동일합니다. 자세한 내용은 here을 참조하십시오.

산술을 사용하기 때문에 어설 션이 효과적으로 명제 프래그먼트에 없습니다. Z3는 다른 조각을 결정할 수 있습니다. Z3 tutorial에는 Z3에서 결정할 수있는 조각 목록이 있습니다. 어설 션은 나열된 조각 중 하나에 포함되어 있지 않지만 Z3은 문제없이 다른 어설 션을 처리 할 수 ​​있어야합니다.

어설 션의 정확성과 관련하여 다음 두 가지 주장을 충족 할 수 없습니다. 우리가 h으로 정량을 인스턴스화하는 경우

(assert (S h)) 
(assert (forall ((y Int)) (=> (S y) (< h y)))) 

우리는 거짓 (< h h)을 추론 할 수있다. 나는 당신이하려는 것을 봅니다. 또한 다음과 같은 간단한 인코딩을 고려할 수도 있습니다 (너무 간단 할 수도 있음). 온라인 here에서도 볼 수 있습니다.

;; Encode a 'list' as a "mapping" from position to value 
(declare-fun list (Int) Int) 

;; Asserting that the list is sorted 
(assert (forall ((i Int) (j Int)) (=> (<= i j) (<= (list i) (list j))))) 

;; Now, we prove that for every i >= 0 the element at position 0 is less than equal to element at position i 
;; That is, we show that the negation is unsatisfiable with the previous assertion 
(assert (not (forall ((i Int)) (=> (>= i 0) (<= (list 0) (list i)))))) 

(check-sat) 

마지막으로 Z3에는 수식이 효과적으로 명제 단편에 있는지 여부를 확인하기위한 명령 줄이 없습니다.