정의 한정 기호 정의

Question

Z3에서 표기법의 반복 최대 값을 사용하는 공식 증명을 확인하려고합니다. 예를 들어, fa 함수 (↑ i :   0 ≤ i < N :   f (i))는 0과 N 사이의 값에 적용될 때 f의 최대 값을 지정합니다.

으로 멋지게 공리화 할 수 있습니다.

(↑ I : P (I) : F (I)) ≤     X     < =>     (∀i :   P (I)   F (I) ≤ X)

와

i의 유형에 대한 술어. Z3에서 그러한 한정 기호를 정의 할 수있는 방법이 있습니까?

가능한 한이 정의에 가깝도록 내 교정본을 공식화하는 것이 매우 편리합니다.

감사합니다.

Answer 1

Z3에서 그러한 바인더를 정의하는 직접적인 방법은 없습니다. Z3은 고전적인 단순 정렬 ​​된 1 차 논리에 기반하며 유일한 결합제는 보편적 및 출구 적 정량입니다. 특히 Z3에서는 람다 식을 직접 작성할 수 없습니다. 중첩 된 바인더를 포함하는 Z3을 사용하는 정리를 증명하는 한 가지 방법은 람다 리프팅을 먼저 적용한 다음 결과로 나오는 1 차 공식을 증명하려고 시도하는 것입니다.

예제에서 상수 max_p_f를 정의하려고합니다. 다음 속성 : 당신이 최대 기능을 적용 할 경우

이

forall i: p(i) => max_p_f >= f(i) 
(exists i: p(i) & max_p_f = f(i)) or (forall i . not p(i)) 

가합니다 (supremum 가정하면 등, 도메인에 정의) 말 각 P, F 조합에 대한 상수를 생성해야합니다.

이러한 기능을 정의하는 것은 고차원 논리의 증명 보조 장치에서 표준입니다. Isabelle theorem 증명 기는 첫 번째 백엔드 (E, 뱀파이어, Z3 등)에 증명 의무를 매핑 할 때 위와 유사한 변환을 적용합니다.