Z3 : 대수 선형 표현

Question

매트릭스와 벡터가 포함 된 표현식의 특성을 증명하고 싶습니다 (크기는 고정적이지만 크기는 고정적 일 수 있음).

나는 식의 결과가 대각 행렬이나 삼각 행렬이, 또는 명확한 긍정적임을 입증 할 예를 들어

... 내가 인코딩 잘 알려진 속성을 원하는이를 위해

및

||x + y|| <= ||x|| + ||y|| 
(A * B) * C = A * (B * C) 
det(A+B) = det(A) + det(B) 
Tr(zA) = z * Tr(A) 
(I + AB)^(-1) = I - A(I + BA)^(-1) * B 
... 

나는 이것을 Z3에서 구현하려고 시도했다. 그러나 간단한 속성의 경우에도 알 수 없거나 시간이 초과됩니다. 나는 배열 이론과 한정어로 시도했다.

이 문제가 SMT 해결사로 해결 될 수 있는지 또는 이러한 종류의 문제에 적합하지 않은지 알고 싶습니다. 작은 모범을 보여줌으로써 힌트를 줄 수 있습니까?

Answer 1

확실히 Z3을 사용하면이 작업을 수행 할 수 있습니다.

작은 예제 here을 만들었습니다.이 예제는 단위 행렬을 정의하고 대각 행렬이라는 것을 의미하며, 그 다음에 항등 행렬이 대각선임을 증명합니다.

따라서 Z3에서 이러한 종류의 작업을 수행 할 수 있습니다. Dafny 또는 F *와 같은 대화 형 증명 기능이있는 Z3 위에 구축 된 도구를 사용하면 더 나은 시간을 가질 수 있습니다.