mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
a7e3a9df5a
Classical syllogism in Z3. Many samples talks about integer, reals. Not much sample available on non integer things.
34 lines
782 B
Python
34 lines
782 B
Python
############################################
|
||
# Copyright (c) Microsoft Corporation. All Rights Reserved.
|
||
#
|
||
# all humans are mortal
|
||
# Socrates is a human
|
||
# so Socrates mortal
|
||
############################################
|
||
|
||
from z3 import *
|
||
|
||
set_param(proof=True)
|
||
|
||
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) == True]
|
||
|
||
|
||
s = Solver()
|
||
s.add(axioms)
|
||
# classical refutation
|
||
s.add(Mortal(socrates) == False)
|
||
|
||
print(s.check()) # prints unsat so socrates is Mortal
|