questions about the Z3 theorem prover

Stream: new members

[Pavel Kulko]

Mario Carneiro said:

Probably not, but you are welcome to try

I'm trying to translate logical clause expressed in First Order Logic into Z3 (Python version). For example, the logical clause may look like this:
exists l.(language(l) & exists n.(name(n) & :op1(n,"English") & :name(l,n)))
which corresponds to the expression in natural language "language is English".
The idea is to be able to translate it into some form of axiom which can be understood by an Automated Theorem Prover such as Z3. And then reuse it for further inference. For example, I can extract knowledge from the axioms if I construct the right query (code in Z3) for it...

I was initially thinking about using Lean for this, but it looks more like an "interactive theorem prover" (which required human in the middle) rather than "automated theorem prover" which can automate logical proofs.

So the ultimate goal is to create a system capable of accumulating formal knowledge and perform some sort of reasoning with it.

[Scott Morrison]

Are you the person who asked https://stackoverflow.com/questions/70090927/how-can-i-convert-logical-clause-to-lean? What's going on with this clause?

[Pavel Kulko]

Scott Morrison said:

Are you the person who asked https://stackoverflow.com/questions/70090927/how-can-i-convert-logical-clause-to-lean? What's going on with this clause?

yes, I asked that question in StackOverflow as well. The guy who answered it then recommended looking towards Z3 (and recommended asking on this forum as well) So here I am :)

[Mario Carneiro]

could you help #xy this problem for us? What are you actually trying to do that resulted in investigating how to render that clause in Z3 / lean?

[Mario Carneiro]

So the ultimate goal is to create a system capable of accumulating formal knowledge and perform some sort of reasoning with it.

What sort of knowledge, and what sort of reasoning? Could you show a not-entirely-trivial example where the automation is value added?

[Mario Carneiro]

I struggle to think of any interesting questions to ask about the clause "language is english" that doesn't already restate the answer in the question

[Pavel Kulko]

Mario Carneiro said:

So the ultimate goal is to create a system capable of accumulating formal knowledge and perform some sort of reasoning with it.

What sort of knowledge, and what sort of reasoning? Could you show a not-entirely-trivial example where the automation is value added?

We can start with answering "surface questions" like "<unknown> is English" or "language is <unknown>" which can find answers from the context of the existing axioms. Then we can try to answer the Yes/No questions like "Is English a language?". Then we can possibly extend it to other types of reasoning, involving many axioms at the same time.

[Pavel Kulko]

The idea is to be able to create a knowledge base which would not only store knowledge but also have a means to reason with it. I tried using Knowledge Graphs for it. But KGs usually don’t have built-in mechanisms for inference. I can retrieve data using SPARLQ queries, for example. But then the problem is how translate natural language question into SPARQL formal query… you have to use some heuristics or machine learning methods to find the correct answer space (best matching sub-graph) and infer the answer from it. But even that approach may not be able to answer questions which require reasoning and logical inference. They can mainly answer the so called “surface questions” where the answers are readily available in the context. So I looked at automated theorem provers. They look like a perfect solution for that task. They store knowledge as “axioms”. They can build further knowledge based on the existing axioms or add new ones. And, unlike KG heuristic search with "fuzzy" results, their answers can be mathematically (logically) sound. So it looks like the way to go…

[Mario Carneiro]

In that case, I think the single clause is(language, english) would do fine for encoding this in an ATP. You might also consider Prolog for answering those forward/backward questions like <unknown> is English

[Pavel Kulko]

Mario Carneiro said:

In that case, I think the single clause is(language, english) would do fine for encoding this in an ATP. You might also consider Prolog for answering those forward/backward questions like <unknown> is English

can you help me translate the whole thing into Z3 ? I mean the axiom itself and the possible query.

[Mario Carneiro]

It depends on the interface you are working with, but maybe https://colab.research.google.com/github/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb will help?

[Pavel Kulko]

Mario Carneiro said:

It depends on the interface you are working with, but maybe https://colab.research.google.com/github/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb will help?

Thanks, I read it through already. But I'm stuck with translation of the axiom. In standard Z3 syntaxis it would look like this:

(declare-const name (String))
(declare-const language (String))
(assert (exists ((l language)) (and (language l) (exists ((n name)) (and (name n) (:op1 n "English") (:name l n))))))

But in Python implementation I try this code, for example:

from z3 import *

Object = DeclareSort('Object')
name = Function('name', Object, BoolSort())
language = Function('language', Object, BoolSort())
op1 = Function('op1', Object, Object, BoolSort())

l = Const('l', Object)
n = Const('n', Object)

s = Solver()
s.add(ForAll(l, Implies(language(l), Exists(n, And(name(n), op1(n, "English"), name(l, n))))))

print(s.check())
print(s.model())

but it gives an error

[Mario Carneiro]

1. You used ForAll instead of Exists, that looks suspicious
2. I don't think you need that axiom / it doesn't say what you want. I don't use python/z3 so I'm projecting syntax but I guess it would be something like:

Object = DeclareSort('Object')
language = Function('language', Object, BoolSort())
english = Const('English', Object)

s = Solver()
s.add(language(english))
print(s.check())
print(s.model())

[Pavel Kulko]

Mario Carneiro said:

1. You used ForAll instead of Exists, that looks suspicious
2. I don't think you need that axiom / it doesn't say what you want. I don't use python/z3 so I'm projecting syntax but I guess it would be something like:

Object = DeclareSort('Object')
language = Function('language', Object, BoolSort())
english = Const('English', Object)

s = Solver()
s.add(language(english))
print(s.check())
print(s.model())

I played more with Z3, and it looks like I can make it answer boolean questions. See example code below:

from z3 import *

Object = DeclareSort('Object')
Languages = DeclareSort('Languages')

Human = Function('Human', Object, BoolSort())
Mortal = Function('Mortal', Object, BoolSort())

socrates = Const('socrates', Object)
pavel = Const('pavel', Object)
Something = Function('Something',  Object, BoolSort())

Whiskers = Function('Whiskers', Object, BoolSort())
Tail = Function('Tail', Object, BoolSort())
Cat = Function('Cat', Object, BoolSort())

Language = Function('Language', Languages, BoolSort())
english = Const('English', Languages)
french= Const('French', Languages)
Name = Function('Name', Languages, BoolSort())

# free variables used in forall must be declared Const in python
x = Const('x', Object)
y = Const('y', Languages)

axioms = [
    ForAll([x],Implies(Human(x), Mortal(x))),
    ForAll([x],Implies(Cat(x), And(Whiskers(x), Tail(x)))),
    ForAll([x],Implies(Cat(x), Not(Human(x)))),
    ForAll([x],Implies(Cat(x), Mortal(x))),
    ForAll([y],Implies(Language(y), And(Name(y))))
]

s = Solver()
s.add(axioms)

assumptions = [
    Cat(socrates),
    Human(pavel),
    #Cat(pavel) # <- this assumption makes model unsat because cat(x) is not human(x)
    Name(english),
    Name(french)
]

if unsat == s.check(assumptions):
    print(f'UNSAT: {s.unsat_core()}')
else:
    print('SAT:\n')
    m = s.model()
    #print(m)
    #print(m.eval(Cat(english))) <- error "sort mismatch"
    print(m.eval(Human(socrates)))
    print(m.eval(And(Mortal(socrates),Tail(socrates))))
    print(m.eval(Tail(socrates)))
    #print(m.eval(Tail(french))) <- error "sort mismatch"

The above code has several axioms and assumptions. Then it generates a model which can be evaluated. So far so good. But how can I make it answer "Wh-questions"? For example, "what languages do you know?" or "how many languages is there?"

[Kyle Miller]

@Pavel Kulko I think you need some actual data types for this to work, since socrates, pavel, english, and french are actually variables (it's just called a Const). To enumerate answers, you can do s.check in a loop, and each time you add in an additional assumption that the variable doesn't equal the value you just got. Here's answering all the mortals in the model:

from z3 import *

Object_ = Datatype('Object')
Object_.declare("socrates")
Object_.declare("pavel")
Object = Object_.create()

Languages_ = Datatype('Languages')
Languages_.declare("English")
Languages_.declare("French")
Languages = Languages_.create()

Human = Function('Human', Object, BoolSort())
Mortal = Function('Mortal', Object, BoolSort())

Something = Function('Something',  Object, BoolSort())

Whiskers = Function('Whiskers', Object, BoolSort())
Tail = Function('Tail', Object, BoolSort())
Cat = Function('Cat', Object, BoolSort())

Language = Function('Language', Languages, BoolSort())
Name = Function('Name', Languages, BoolSort())

# free variables used in forall must be declared Const in python
x = Const('x', Object)
y = Const('y', Languages)

axioms = [
    ForAll([x],Implies(Human(x), Mortal(x))),
    ForAll([x],Implies(Cat(x), And(Whiskers(x), Tail(x)))),
    ForAll([x],Implies(Cat(x), Not(Human(x)))),
    ForAll([x],Implies(Cat(x), Mortal(x))),
    ForAll([y],Implies(Language(y), And(Name(y))))
]

s = Solver()
s.add(axioms)

assumptions = [
    Cat(Object.socrates),
    Human(Object.pavel),
    #Cat(Object.pavel), # <- this assumption makes model unsat because cat(x) is not human(x)
    Name(Languages.English),
    Name(Languages.French)
]

s.push()

s.add(assumptions)

v = Const('v', Object)
s.add(Mortal(v))

while s.check() == sat:
    m = s.model()
    print("v = %s" % m[v])
    s.add(v != m[v])

s.pop()

[Pavel Kulko]

That works nicely! Thank you @Kyle Miller Now that we are able to answer simple Wh-queries, what about more complex ones? Can we return a clause, for example? Lets say I want to ask "what does cat have?" And it should return "And(Whiskers(x), Tail(x))". Can we do that?

[Mario Carneiro]

@Pavel Kulko That query sounds very ambiguous. Why is it not returning [Whiskers(x), Tail(x), Not(Human(x)), Mortal(x)]?

[Pavel Kulko]

Mario Carneiro said:

Pavel Kulko That query sounds very ambiguous. Why is it not returning [Whiskers(x), Tail(x), Not(Human(x)), Mortal(x)]?

Well, the code below returns constant "v = socrates". But how can I make it return some clause?

v = Const('v', Object)
s.add(Cat(v))

while s.check() == sat:
    m = s.model()
    print("v = %s" % m[v])
    s.add(v != m[v])

[Mario Carneiro]

what clause?

[Mario Carneiro]

the question isn't uniquely determined; there are an infinite number of clauses that are true about anything satisfying Cat(x)

[Pavel Kulko]

Mario Carneiro said:

the question isn't uniquely determined; there are an infinite number of clauses that are true about anything satisfying Cat(x)

In this case we should only return the clause (or part of it) which was provided in the axioms.. or maybe I should formulate the question differently. Currently I can extract all the satisfying predicates from the model based on the appearance of the variable "socrates" in the else_value(): [Whiskers(x), Cat(x), Tail(x), Mortal(x)].

[Mario Carneiro]

If you have a list of candidate formulas, you can see which ones are derivable from Cat(x) by seeing if Cat(x) => P is derivable

[Pavel Kulko]

Mario Carneiro said:

If you have a list of candidate formulas, you can see which ones are derivable from Cat(x) by seeing if Cat(x) => P is derivable

yes, that could work. I'm just trying different query now. For example s.add(Implies(Tail(v),Human(v))) will return constant "pavel". But what I'm trying to ask with this clause is "does the human have tail?" Is the clause formulated correctly?

[Mario Carneiro]

You need a quantifier. Do you mean to ask whether any human has a tail or all?

[Pavel Kulko]

Mario Carneiro said:

You need a quantifier. Do you mean to ask whether any human has a tail or all?

Thanks. Indeed, this query works s.add(ForAll([v],Implies(Tail(v),Human(v))))

[Pavel Kulko]

Pavel Kulko said:

Mario Carneiro said:

You need a quantifier. Do you mean to ask whether any human has a tail or all?

Thanks. Indeed, this query works s.add(ForAll([v],Implies(Tail(v),Human(v))))

what if I want to ask "is pavel mortal"? How can I encode it?

[Mario Carneiro]

add Mortal(pavel) and see if it is unsat, and similarly for !Mortal(pavel):

• If adding Mortal(pavel) makes it unsat, then pavel is immortal
• If adding !Mortal(pavel) makes it unsat, then pavel is mortal
• If neither makes it unsat, then the given axioms are not enough to determine whether pavel is mortal or not

[Pavel Kulko]

Pavel Kulko said:

Pavel Kulko said:

Mario Carneiro said:

You need a quantifier. Do you mean to ask whether any human has a tail or all?

Thanks. Indeed, this query works s.add(ForAll([v],Implies(Tail(v),Human(v))))

what if I want to ask "is pavel mortal"? How can I encode it?

Would it be enough to just add s.add(Mortal(Object.pavel)) and then check if the solver returns "sat" ? So that would mean true. Otherwise, if it returns "unsat" then it is either False or Unknown?

[Mario Carneiro]

Not quite. Notice that I said to look for "unsat", not "sat". If adding Mortal(pavel) returns "sat" that doesn't mean that pavel is mortal, it means that we cannot exclude the possibility that pavel is mortal

[Mario Carneiro]

to prove that pavel is mortal we instead want to add !Mortal(pavel) and get a contradiction

[Pavel Kulko]

ah ok, and to check if the answer is Unknown we just need to run it two times, once with the original query and the second time with the negated query. If both original and negated query return "sat" then the answer is unknown. is that correct?

[Mario Carneiro]

yes, although it's more like "independent" than "unknown". "Unknown" would be if you got at least one "Unknown" response to those queries, which means the sat solver couldn't prove or disprove the assertion within the time limit

[Pavel Kulko]

How can I answer the question "who is pavel"? That is, given the constant (Object.pavel), I want to find all the predicates where this constant can be applied.

[Pavel Kulko]

currently I'm solving that problem by evaluating all the predicates known by the model.

for decl in m.decls():
                interp = m.get_interp(decl)
                if isinstance(interp, FuncInterp):
                    try:
                        #check if predicate can be evaluated with the constant argument
                        m.eval(decl(const))
                        predicates.append(decl)
                        is_sat = True
                    except:
                        print(f'{decl} != {const}')

But is this the only way? It doesn't seem to be very efficient.

[Mario Carneiro]

It sounds like you just want a list of all predicates which have an argument of type Object. I don't know if Z3's object representation is optimized for that, but probably if you can get all the decls you can ask what their types are and whether one of them is Object

[Aaron Bies]

Is there some way to figure out what z3 does for a specific SMT instance?

I have a set of problems that vary in size, and I tried to find solutions for them using z3. In my tests, I noticed that z3 is absurdly fast for smaller problems but then hits a brick wall at some point. For problem sizes 2 to 11, it takes about 40ms to 50ms to find a solution, but for size 12 it doesn't find anything within an hour.

What I think is happening is that z3 has multiple strategies for solving these SMT instances and it chooses the wrong one for those problems with size 12 and above. So is there a way for me to tell what strategy it's using for a given SMT instance? If so, is there a way for me to force it to use a strategy I know to be effective?

[Mario Carneiro]

Just an FYI, this isn't a forum for Z3 questions

[Aaron Bies]

Do you know of a forum for z3? I tried looking for one, but didn't find anything

[Mario Carneiro]

There is https://github.com/Z3Prover/z3/discussions, no idea whether that is the best place for it but I'm sure asking there will find a better place if there is one

[Aaron Bies]

Alright, I'll repost my question there