Use this Skill for formal logic and automated reasoning: Z3 SMT solver for propositional/first-order logic, modal logic S5, SAT problem encoding, and Lean4 proof verification.
Use this Skill for formal logic and automated reasoning: Z3 SMT solver for propositional/first-order logic, modal logic S5, SAT problem encoding, and Lean4 proof verification.
TL;DR — Use the Z3 SMT solver for propositional and first-order logic, encode
constraint satisfaction puzzles (Zebra/Einstein riddle, N-Queens) as SAT problems,
reason about modal logic S5 validity using Kripke frame semantics, and verify logical
equivalences and tautologies with sympy.
When to Use
Use this Skill when you need to:
Verify whether a logical formula is a tautology, contradiction, or contingency
Encode first-order logic (FOL) theories and check satisfiability
Validate philosophical arguments by formalizing them in propositional or modal logic
Check logical equivalences and argue about modal operators (necessity □, possibility ◇)
Do not use this Skill for:
Probabilistic reasoning under uncertainty (use PyMC or pgmpy)
Natural language argument parsing without formalization (see argument-mapping Skill)
Full higher-order logic or dependent type systems (use Coq or Agda)
Background
Z3 is Microsoft Research's high-performance SMT (Satisfiability Modulo Theories) solver.
It handles propositional logic, linear arithmetic (integers and reals), bit vectors,
arrays, and quantified first-order logic. Key functions:
Z3 API
Description
Bool(name)
Declare a Boolean variable
Int(name), Real(name)
Arithmetic variables
And, Or, Not, Implies, Xor
Logical connectives
ForAll, Exists
First-order quantifiers
Function(name, sort, sort)
Uninterpreted function declaration
Solver.add(constraint)
Assert a formula
Solver.check()
Returns sat, unsat, or unknown
Solver.model()
Extract satisfying assignment
Modal logic S5 is the standard system for epistemic and alethic necessity.
A formula is S5-valid if it holds in every world of every Kripke frame where
the accessibility relation R is an equivalence relation (reflexive, symmetric, transitive).
sympy's logic module (to_cnf, satisfiable, tautology) provides symbolic
manipulation without external solvers, useful for smaller formulas and teaching purposes.
Environment Setup
# Create Python environment
conda create -n formal-logic python=3.11 -y
conda activate formal-logic
# Install dependencies
pip install "z3-solver>=4.12""sympy>=1.12""numpy>=1.23"# Verify Z3
python -c "import z3; print(z3.get_version_string())"# Optional: Lean 4 for proof verification# Install via elan (Lean version manager):# curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh# lake new myproject && cd myproject
from z3 import (
Bool, Int, Solver, And, Or, Not, Implies, Distinct, sat,
Function, IntSort, BoolSort, ForAll, Exists, Real, If
)
defsolve_einstein_riddle() -> dict:
"""
Solve the Einstein/Zebra riddle using Z3 integer constraints.
Five houses in a row; each has a unique nationality, colour, pet, drink, cigarette.
Constraints encode all 15 clues. Return the satisfying assignment.
Returns:
Dict mapping house positions (1-5) to their attribute values.
"""
s = Solver()
# Attributes: each value 1-5 represents the house position
Brit = Int("Brit"); Swede = Int("Swede"); Dane = Int("Dane")
Norwegian = Int("Norwegian"); German = Int("German")
Red = Int("Red"); Green = Int("Green"); White = Int("White")
Yellow = Int("Yellow"); Blue = Int("Blue")
Tea = Int("Tea"); Coffee = Int("Coffee"); Milk = Int("Milk")
Beer = Int("Beer"); Water = Int("Water")
PallMall = Int("PallMall"); Dunhill = Int("Dunhill")
Blends = Int("Blends"); BlueMaster = Int("BlueMaster"); Prince = Int("Prince")
Dog = Int("Dog"); Birds = Int("Birds"); Cats = Int("Cats")
Horse = Int("Horse"); Fish = Int("Fish")
all_vars = [
Brit, Swede, Dane, Norwegian, German,
Red, Green, White, Yellow, Blue,
Tea, Coffee, Milk, Beer, Water,
PallMall, Dunhill, Blends, BlueMaster, Prince,
Dog, Birds, Cats, Horse, Fish,
]
# Domain constraints: each attribute occupies a position 1-5for v in all_vars:
s.add(v >= 1, v <= 5)
# Uniqueness within each category
s.add(Distinct(Brit, Swede, Dane, Norwegian, German))
s.add(Distinct(Red, Green, White, Yellow, Blue))
s.add(Distinct(Tea, Coffee, Milk, Beer, Water))
s.add(Distinct(PallMall, Dunhill, Blends, BlueMaster, Prince))
s.add(Distinct(Dog, Birds, Cats, Horse, Fish))
# Clues
s.add(Brit == Red) # 1. Brit lives in Red house
s.add(Swede == Dog) # 2. Swede keeps Dogs
s.add(Dane == Tea) # 3. Dane drinks Tea
s.add(Green == White - 1) # 4. Green is left of White
s.add(Green == Coffee) # 5. Green owner drinks Coffee
s.add(PallMall == Birds) # 6. PallMall smoker keeps Birds
s.add(Yellow == Dunhill) # 7. Yellow owner smokes Dunhill
s.add(Milk == 3) # 8. Middle house drinks Milk
s.add(Norwegian == 1) # 9. Norwegian lives in first house
s.add(Or(Blends - Cats == 1, Cats - Blends == 1)) # 10. Blends next to Cats
s.add(Or(Horse - Dunhill == 1, Dunhill - Horse == 1)) # 11. Horse next to Dunhill
s.add(BlueMaster == Beer) # 12. BlueMaster smoker drinks Beer
s.add(German == Prince) # 13. German smokes Prince
s.add(Or(Norwegian - Blue == 1, Blue - Norwegian == 1)) # 14. Norwegian next to Blue
s.add(Or(Blends - Water == 1, Water - Blends == 1)) # 15. Blends next to Water
result = s.check()
if result != sat:
return {"error": "No solution found"}
model = s.model()
assignment = {str(v): model.eval(v).as_long() for v in all_vars}
# Determine fish owner (the riddle question)
fish_pos = assignment["Fish"]
owner = next(
name for name in ["Brit", "Swede", "Dane", "Norwegian", "German"]
if assignment[name] == fish_pos
)
assignment["_fish_owner"] = owner
return assignment
defcheck_tautology(formula_str: str) -> dict:
"""
Check whether a propositional formula is a tautology using Z3.
A formula F is a tautology iff ¬F is unsatisfiable.
Args:
formula_str: A description of the formula (handled via Z3 API in caller).
Returns:
Dict with is_tautology (bool), is_satisfiable (bool), is_contradiction (bool).
"""# This function demonstrates the tautology-check pattern.# Callers construct the Z3 formula and pass it directly.raise NotImplementedError(
"Build your formula with Z3 API (Bool, And, Or, ...) then call check_formula_type()."
)
defcheck_formula_type(formula) -> dict:
"""
Determine whether a Z3 formula is a tautology, contradiction, or contingency.
Args:
formula: Any Z3 BoolRef expression.
Returns:
Dict with keys: is_tautology, is_contradiction, is_contingent,
satisfying_model (dict or None).
"""# Check satisfiability of the formula
s_sat = Solver()
s_sat.add(formula)
sat_result = s_sat.check()
# Check satisfiability of its negation (for tautology)
s_neg = Solver()
s_neg.add(Not(formula))
neg_result = s_neg.check()
is_satisfiable = sat_result == sat
neg_satisfiable = neg_result == sat
model = Noneif is_satisfiable:
raw_model = s_sat.model()
model = {str(d): str(raw_model[d]) for d in raw_model.decls()}
return {
"is_tautology": is_satisfiable andnot neg_satisfiable,
"is_contradiction": not is_satisfiable,
"is_contingent": is_satisfiable and neg_satisfiable,
"is_satisfiable": is_satisfiable,
"satisfying_model": model,
}
defcheck_logical_equivalence(formula_a, formula_b) -> bool:
"""
Check whether two Z3 formulas are logically equivalent.
A ≡ B iff (A ↔ B) is a tautology, i.e., ¬(A ↔ B) is unsatisfiable.
Args:
formula_a: First Z3 BoolRef.
formula_b: Second Z3 BoolRef.
Returns:
True if the formulas are equivalent, False otherwise.
"""from z3 import Xor
biconditional = Not(Xor(formula_a, formula_b))
result = check_formula_type(biconditional)
return result["is_tautology"]
Step 2 — First-Order Logic and Function Declaration
deffol_example_socrates() -> dict:
"""
Encode and verify the classic syllogism in Z3 first-order logic.
Premises:
1. All men are mortal: ForAll x. Man(x) → Mortal(x)
2. Socrates is a man: Man(Socrates)
Conclusion:
Socrates is mortal: Mortal(Socrates)
Returns:
Dict with is_valid (bool) and explanation.
"""from z3 import DeclareSort, Const, Function, BoolSort, ForAll, Implies, And, Not, Solver, sat
# Declare domain sort
Person = DeclareSort("Person")
# Declare predicates
Man = Function("Man", Person, BoolSort())
Mortal = Function("Mortal", Person, BoolSort())
# Declare constants
Socrates = Const("Socrates", Person)
x = Const("x", Person)
# Premises
all_men_mortal = ForAll(x, Implies(Man(x), Mortal(x)))
socrates_is_man = Man(Socrates)
# Conclusion (negate to check validity)
conclusion = Mortal(Socrates)
# Valid iff premises ∧ ¬conclusion is unsat
s = Solver()
s.add(all_men_mortal)
s.add(socrates_is_man)
s.add(Not(conclusion))
result = s.check()
is_valid = result != sat # UNSAT means the argument is validreturn {
"is_valid": is_valid,
"explanation": "The syllogism is valid: premises entail the conclusion."if is_valid else"Unexpected: premises do not entail conclusion.",
}
defsolve_nqueens(n: int = 8) -> list[int]:
"""
Solve the N-Queens problem using Z3 constraint satisfaction.
Each queen is placed at column q[i] in row i.
Constraints: all columns distinct, no diagonal attacks.
Args:
n: Board size (n×n).
Returns:
List of column positions [q_0, q_1, ..., q_{n-1}], or empty list if unsat.
"""
queens = [Int(f"q_{i}") for i inrange(n)]
s = Solver()
# Domainfor q in queens:
s.add(q >= 0, q < n)
# All columns distinct
s.add(Distinct(queens))
# No diagonal attacksfor i inrange(n):
for j inrange(i + 1, n):
s.add(queens[i] - queens[j] != i - j)
s.add(queens[i] - queens[j] != j - i)
if s.check() == sat:
model = s.model()
return [model.eval(queens[i]).as_long() for i inrange(n)]
return []
Step 3 — Modal Logic S5 Validity Check
defcheck_s5_validity(
formula_fn,
n_worlds: int = 4,
verbose: bool = False,
) -> dict:
"""
Check whether a modal formula is valid in S5 using a brute-force Kripke model.
In S5, the accessibility relation R is an equivalence relation (reflexive,
symmetric, transitive), which means every world accesses every other world.
A formula is S5-valid iff it holds in ALL worlds of ALL possible valuations.
This function tests validity by checking whether the negation is satisfiable
in any Kripke model with `n_worlds` worlds (complete graph accessibility for S5).
Args:
formula_fn: A function (worlds, R, V, w) → bool, where worlds is a list
of world indices, R is the accessibility relation set of pairs,
V is a dict {prop: set of worlds where prop is true}, and w is
the current evaluation world.
n_worlds: Number of worlds in the Kripke frame.
verbose: If True, print counterexample valuations when found.
Returns:
Dict with is_valid (bool), counterexample (dict or None).
"""import itertools
worlds = list(range(n_worlds))
# S5: universal accessibility (every world sees every world)
R = {(w1, w2) for w1 in worlds for w2 in worlds}
# Generate all possible valuations for one propositional variable p# (2^n_worlds valuations; extend for multiple variables as needed)for truth_combo in itertools.product([True, False], repeat=n_worlds):
V = {"p": {w for w, val inenumerate(truth_combo) if val}}
# Check formula holds in all worldsfor w in worlds:
holds = formula_fn(worlds, R, V, w)
ifnot holds:
if verbose:
print(f"Counterexample found: V(p)={V['p']}, world={w}")
return {
"is_valid": False,
"counterexample": {
"V_p": list(V["p"]),
"falsified_at_world": w,
},
}
return {"is_valid": True, "counterexample": None}
defmodal_necessity(worlds, R, V, w, prop="p"):
"""□p: p holds in all accessible worlds (R[w])."""
accessible = {v for (u, v) in R if u == w}
returnall(v in V.get(prop, set()) for v in accessible)
defmodal_possibility(worlds, R, V, w, prop="p"):
"""◇p: p holds in some accessible world."""
accessible = {v for (u, v) in R if u == w}
returnany(v in V.get(prop, set()) for v in accessible)
Advanced Usage
sympy Propositional Logic
from sympy.logic.boolalg import to_cnf, Equivalent, Implies as Imp
from sympy.logic.inference import satisfiable
from sympy import symbols
defsympy_tautology_check(formula) -> bool:
"""
Check if a sympy Boolean formula is a tautology.
A formula is a tautology iff its negation is unsatisfiable.
Args:
formula: sympy Boolean expression.
Returns:
True if tautology, False otherwise.
"""from sympy import Not
neg = Not(formula)
result = satisfiable(neg)
return result isFalsedefdemonstrate_de_morgan() -> None:
"""Show that De Morgan's laws are tautologies using sympy."""
A, B = symbols("A B")
# ¬(A ∧ B) ↔ (¬A ∨ ¬B)
law1 = Equivalent(~(A & B), (~A | ~B))
# ¬(A ∨ B) ↔ (¬A ∧ ¬B)
law2 = Equivalent(~(A | B), (~A & ~B))
print(f"De Morgan law 1 is tautology: {sympy_tautology_check(law1)}")
print(f"De Morgan law 2 is tautology: {sympy_tautology_check(law2)}")
print(f"CNF of ¬(A → B): {to_cnf(~Imp(A, B))}")
Troubleshooting
Problem
Cause
Fix
z3.z3types.Z3Exception: unknown
Quantified formula with non-linear arithmetic
Use linear arithmetic only; avoid multiplying Z3 variables
Z3 check() returns unknown on timeout
Undecidable theory fragment
Set s.set("timeout", 5000) (ms); simplify constraints
Distinct() with one variable
Z3 requires ≥2 arguments
Wrap in a list check before calling Distinct()
sympy satisfiable() returns {} not False
Tautology returns empty model
Empty dict {} means tautology (no variable assignment falsifies it)
N-Queens unsat for n=2 or n=3
No valid placement exists
n=2 and n=3 are mathematically unsolvable; try n≥4
# Solve the Einstein/Zebra riddle
solution = solve_einstein_riddle()
print(f"Fish is owned by: {solution['_fish_owner']}")
print(f"Fish house position: {solution['Fish']}")
# Check a tautology: A → (B → A) (Axiom K of propositional logic)
A = Bool("A")
B = Bool("B")
formula_k = Implies(A, Implies(B, A))
result = check_formula_type(formula_k)
print(f"\nFormula A → (B → A) is tautology: {result['is_tautology']}")
# Check equivalence: ¬(A → B) ↔ (A ∧ ¬B)
lhs = Not(Implies(A, B))
rhs = And(A, Not(B))
equiv = check_logical_equivalence(lhs, rhs)
print(f"¬(A → B) ≡ (A ∧ ¬B): {equiv}")
# Solve 8-Queens
queens_solution = solve_nqueens(8)
print(f"\n8-Queens solution: {queens_solution}")
Example 2 — FOL Syllogism and Modal S5 Validity
# Verify the Socrates syllogism in FOL
fol_result = fol_example_socrates()
print(f"Socrates syllogism valid: {fol_result['is_valid']}")
print(fol_result["explanation"])
# Check S5 axiom: □p → p (T axiom: what is necessary is actual)deft_axiom(worlds, R, V, w):
"""□p → p: if p is necessary at w, then p holds at w."""
box_p = modal_necessity(worlds, R, V, w, prop="p")
p_at_w = w in V.get("p", set())
return (not box_p) or p_at_w # material implication
t_result = check_s5_validity(t_axiom, n_worlds=4, verbose=True)
print(f"\nS5 T-axiom (□p → p) is valid: {t_result['is_valid']}")
# Check S5 axiom: ◇p → □◇p (5 axiom: what is possible is necessarily possible)defaxiom_5(worlds, R, V, w):
"""◇p → □◇p"""
poss_p = modal_possibility(worlds, R, V, w, prop="p")
accessible = {v for (u, v) in R if u == w}
box_poss_p = all(
modal_possibility(worlds, R, V, v, prop="p") for v in accessible
)
return (not poss_p) or box_poss_p
a5_result = check_s5_validity(axiom_5, n_worlds=4)
print(f"S5 Axiom 5 (◇p → □◇p) is valid: {a5_result['is_valid']}")
# Demonstrate De Morgan's laws
demonstrate_de_morgan()
