1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
############################################
# Copyright (c) Microsoft Corporation. All Rights Reserved.
#
# all humans are mortal
# Socrates is a human
# so Socrates mortal
############################################
from z3 import *
Object = DeclareSort('Object')
Human = Function('Human', Object, BoolSort())
Mortal = Function('Mortal', Object, BoolSort())
# a well known philosopher
socrates = Const('socrates', Object)
# free variables used in forall must be declared Const in python
x = Const('x', Object)
axioms = [ForAll([x], Implies(Human(x), Mortal(x))),
Human(socrates)]
s = Solver()
s.add(axioms)
print(s.check()) # prints sat so axioms are coherent
# classical refutation
s.add(Not(Mortal(socrates)))
print(s.check()) # prints unsat so socrates is Mortal
|
