Z3 Prover (привязки Python) не может определить отрицательный Modus Ponens, когда proof = True - PullRequest
Новая
       24

Z3 Prover (привязки Python) не может определить отрицательный Modus Ponens, когда proof = True

0 голосов
/ 16 марта 2019

Я пытаюсь понять, почему Solver Z3 возвращает «неизвестно», когда пытается удовлетворить следующий несовместимый набор выражений. 

In [1]: from z3 import *

In [2]: set_param(proof=True)

In [3]: s = Solver()

In [4]: p,q = Bools("p q")

In [5]: s.add(p)

In [6]: s.add(Not(q))

In [7]: s.add(Implies(p,q))

In [8]: s.check()
Out[8]: unknown

Обратите внимание, что мы не получаем «неизвестно», когда не установленпараметр доказательства к True 

In [1]: from z3 import *

In [2]: s = Solver()

In [3]: p,q = Bools("p q")

In [4]: s.add(p)

In [5]: s.add(Not(q))

In [6]: s.add(Implies(p,q))

In [7]: s.check()
Out[7]: unsat

Кроме того, мы не получаем «неизвестность», когда используем другой несовместимый набор выражений, даже когда устанавливаем proof = True: 

In [1]: from z3 import *

In [2]: set_param(proof=True)

In [3]: s = Solver()

In [4]: x = Int('x')

In [5]: s.add(x==0)

In [6]: s.add(x>0)

In [7]: s.check()
Out[7]: unsat

Что такоепроблематично настроить этот несовместимый набор выражений в логике предложения, в то время как параметр доказательства установлен в True?

...