Everything you need to build with UniLog.

01 Introduction

What UniLog is

UniLog is a modular, fibred logic framework. It lets you express constraints that span multiple logical paradigms — temporal, epistemic, deontic, probabilistic, fuzzy, and so on — within a single formal language, with a single evaluation engine, and with formal guarantees that adding a paradigm does not change the meaning of constraints written in another.

If you have ever found yourself writing “the system must always alert a physician within 5 minutes of a critical lab result, provided the physician has permission to view the result, and with probability at least 0.95 under normal conditions” — that is a UniLog-style constraint. The temporal, deontic, and probabilistic aspects all live in the same formula, evaluated against the same model.

Who this guide is for

• System architects specifying constraints for COH or CZOA-based systems.
• Researchers implementing or extending UniLog.
• Developers integrating UniLog into a larger toolkit such as CZOI.
• Students learning how to combine logical paradigms in a disciplined way.

How to use this guide

• Read Parts I and II in order if you are new to the toolkit.
• Use Part III as a reference for building models.
• Part IV is organised by logic module — read the sections relevant to your problem.
• Part V covers verification and applications.
• Part VI is for extension and troubleshooting.

02 Installation and setup

Requirements

• Python: 3.9 or later (3.10+ recommended).
• Core: antlr4-python3-runtime >= 4.9, numpy >= 1.19.
• Optional: z3-solver for SMT verification; clingo for ASP-based defaults.

Installing from source

git clone https://github.com/hongxueharriswang/unilog_toolkit.git
cd unilog_toolkit
pip install -e .

Optional integrations

pip install -e ".[smt]"       # Z3 integration
pip install -e ".[clingo]"    # Clingo integration
pip install -e ".[dev]"       # pytest, hypothesis

Verifying the installation

from unilog.parser import UniLangParser
from unilog.engine import InferenceEngine

parser = UniLangParser()
phi = parser.parse_string("p -> p")
print(phi)
# Implies(left=Atom(name='p', args=()), right=Atom(name='p', args=()))

If the import succeeds and the formula prints, the installation is correct.

Environment variables

First import

from unilog.parser import UniLangParser        # parsing
from unilog.engine import (                    # reasoning
    InferenceEngine, Model, World,
    ClassicalSolver, ModalSolver, TemporalSolver,
    default_solvers, SMTSolver,
)
from unilog import ast                         # AST node classes

Everything else is internal and may change between minor versions.

03 Core concepts

Five ideas structure everything else in the toolkit: formulas, worlds, models, solvers, and the engine.

Formulas

A formula is a syntactic object — the abstract syntax tree returned by the parser. Formulas do not, on their own, have truth values. They have structure.

from unilog.parser import UniLangParser
phi = UniLangParser().parse_string("G(p -> F q)")

The result is an AST node of type GFormula whose sub field is an Implies whose left is Atom("p") and whose right is an FFormula containing Atom("q"). Formulas are immutable and hashable.

Worlds

A world (or state) is a point at which a formula is evaluated. Worlds are opaque identifiers wrapped in the World class:

from unilog.engine import World
s0 = World(0)
s1 = World("critical")

The wrapper distinguishes world identifiers from other values (constants, numbers, subterms) during evaluation.

Models

A model provides the semantic structures that give formulas meaning: which worlds exist, which atoms are true where, which worlds are accessible from which others, what the domain of individuals is, and so on.

A model is a Python object that subclasses unilog.engine.Model. It does not need to provide every structure — only the ones used by the formulas you evaluate.

Solvers

A solver knows how to evaluate one family of operators. There are eleven solvers in v2.0, one per module. Each implements:

def supports(self, formula) -> bool: ...
def evaluate(self, formula, model, world, assignment) -> bool: ...

The engine

The InferenceEngine is a singleton that dispatches formulas to solvers. You do not normally call solvers directly. You call:

engine.evaluate(phi, model, world, assignment=None)

The engine walks the AST top-down, finds the solver that supports the top node, and delegates. Recursive subformulas re-enter the engine via the same entry point.

04 Your first formula

A minimal example

from unilog.parser import UniLangParser
from unilog.engine import InferenceEngine, Model, World

class TrivialModel(Model):
    def worlds(self):        return {World(0)}
    def valuation(self, w, atom, args):    return atom == "p"
    def accessibility(self, w, modality, agent=None): return set()
    def domain(self):        return set()
    def interpret(self, term, assignment): return None
    def probability(self, world, event):   return 0.0
    def preference(self, world, w1, w2):   return False

parser = UniLangParser()
engine = InferenceEngine.get_instance()

phi = parser.parse_string("p -> p")
print(engine.evaluate(phi, TrivialModel(), World(0)))   # True

Three things happened:

1. The parser turned the string into an AST.
2. A model was constructed with a single world where p is true.
3. The engine dispatched the formula to ClassicalSolver.

A formula that fails

phi = parser.parse_string("p & ~p")
print(engine.evaluate(phi, TrivialModel(), World(0)))   # False

A formula with modalities

class TwoWorlds(Model):
    def __init__(self):
        self.s0, self.s1 = World(0), World(1)
    def worlds(self):    return {self.s0, self.s1}
    def valuation(self, w, atom, args):
        return atom == "p" and w == self.s1
    def accessibility(self, w, modality, agent=None):
        return {self.s1}
    def domain(self):    return set()
    def interpret(self, term, assignment): return None
    def probability(self, world, event):   return 0.0
    def preference(self, world, w1, w2):   return False

phi = parser.parse_string("[]p")
print(engine.evaluate(phi, TwoWorlds(), World(0)))   # True

05 Syntax reference

UniLang accepts both ASCII and Unicode. Every operator has at least one ASCII form, so formulas are always writable on any keyboard.

Classical connectives

Modal and epistemic

Deontic

Temporal

Dynamic logic

Description logic

Probabilistic, non-monotonic, preference, fuzzy

The norm strings are "G" (Gödel, default), "L" (Łukasiewicz), and "P" (Product).

Comments and precedence

Comments use -- line or /* block */.

From lowest to highest precedence: ↔, →, =>, ≺, ∨, ∧, then prefix operators. Use parentheses when in doubt.

06 Writing formulas by hand

The four constraint patterns

Invariant

A property that must hold in every state:

G(invariant_condition)

Example: every zone is contained in its parent.

phi = parser.parse_string(
    "G(forall u (inZone(u, z) -> inZone(u, parent(z))))")

Trigger

An event that causes an action under a condition:

G(event & condition -> X action)

Example: a critical lab result triggers a physician alert.

phi = parser.parse_string(
    "G(labResult(p, r) & critical(r) -> X(alertPhysician(p)))")

Goal

An optimisation objective:

Opt(phi)         # maximise phi
phi ≺ psi        # phi is preferred to psi

Example: minimising mortality.

phi = parser.parse_string(
    "forall r1, r2 (mortalityRate(r1) ≺ mortalityRate(r2) <-> r1 < r2)")

Access

A permission, obligation, or prohibition:

P(do(u, op))       # permitted
O(do(u, op))       # obligatory
Forb(do(u, op))    # forbidden

Example: separation of duty.

phi = parser.parse_string(
    "Forb(prescribe(u, m) & dispense(u, m))")

Combining paradigms

UniLog formulas freely mix paradigms:

phi = parser.parse_string(
    "G(K_alice(critical(p, r)) -> O(X(alertPhysician(p))))")

Read: “always, if Alice knows the result is critical for patient p, then it is obligatory that in the next state a physician is alerted for p.”

phi = parser.parse_string(
    "P_>=0.95(G(request -> F_[0,5] response))")

Read: “with probability at least 0.95, every request is followed within 5 time units by a response.”

Common mistakes

07 The Model interface

Required methods

Every model subclasses unilog.engine.Model and implements seven methods. These are the minimum needed for the engine to evaluate any formula.

If your formulas do not use a structure, its method should return the trivial value (set(), 0.0, False).

Optional methods

Design guidance

• Keep models small. A model is a witness for the formula you want to check, not a simulation of the whole system.
• Use dictionary-backed patterns. Store valuations, accessibility, and other relations in dictionaries keyed by (world, ...). Fast, transparent, easy to serialise.
• Prefer composition over inheritance. Extract shared structure into helpers or small base classes.
• Document what your model means. A comment on each model class explaining its worlds, atoms, and relations pays off immediately.

08 Building models: a walkthrough

A complete model for a small hospital alerting system.

The scenario

A lab system produces results. Some are critical. When a critical result arrives, the attending physician must be alerted within the next state. We model three moments:

• s0 — before the critical result.
• s1 — the critical result has arrived.
• s2 — the physician has been alerted.

Complete class

from unilog.engine import Model, World

class Hospital(Model):
    def __init__(self):
        self.s0 = World(0); self.s1 = World(1); self.s2 = World(2)
        self._states = [self.s0, self.s1, self.s2]
        self._vals = {
            (self.s1, "critical", ("p1",)): True,
            (self.s2, "alerted",  ("p1",)): True,
        }
        self._next = {self.s0: {self.s1},
                      self.s1: {self.s2},
                      self.s2: set()}
        self._deontic = {s: {s} for s in self._states}
        self._domain = {"p1"}

    def worlds(self):
        return set(self._states)

    def valuation(self, w, atom, args):
        return self._vals.get((w, atom, tuple(args)), False)

    def accessibility(self, w, modality, agent=None):
        if modality == "X":     # temporal next
            return self._next.get(w, set())
        if modality == "O":     # deontic
            return self._deontic.get(w, set())
        return set()

    def current_path(self, w):
        return [self.s0, self.s1, self.s2] if w == self.s0 else None

    def domain(self):
        return set(self._domain)

    def interpret(self, term, assignment):
        from unilog import ast
        if isinstance(term, ast.Constant): return term.value
        if isinstance(term, ast.Variable): return assignment.get(term.name)
        return None

    def probability(self, world, event):
        return 0.0

    def preference(self, world, w1, w2):
        return False

Evaluating constraints

from unilog.parser import UniLangParser
from unilog.engine import InferenceEngine

parser = UniLangParser()
engine = InferenceEngine.get_instance()
model = Hospital()

# Invariant: whenever a patient is critical, they are alerted next
phi1 = parser.parse_string(
    "G(forall p (critical(p) -> X(alerted(p))))")
print(engine.evaluate(phi1, model, model.s0))   # True

# Trigger-style: critical result leads to an alert
phi2 = parser.parse_string(
    "G(critical(p1) -> X(alerted(p1)))")
print(engine.evaluate(phi2, model, model.s0))   # True

# Deontic: obligation to alert in the next state
phi3 = parser.parse_string(
    "G(critical(p1) -> O(X(alerted(p1))))")
print(engine.evaluate(phi3, model, model.s0))   # True

09 Model patterns for common scenarios

Linear-time pattern

For LTL and trigger constraints, use a linear chain of worlds:

class LinearTime(Model):
    def __init__(self, n_states):
        self.states = [World(i) for i in range(n_states)]
    def worlds(self):
        return set(self.states)
    def accessibility(self, w, modality, agent=None):
        if modality == "X":
            i = self.states.index(w)
            return {self.states[i+1]} if i+1 < len(self.states) else set()
        return set()
    def current_path(self, w):
        return list(self.states) if w == self.states[0] else None
    # ... other required methods

Branching-time pattern

For CTL and “there exists a path” properties, use a tree or DAG:

class Branching(Model):
    def __init__(self):
        self.s0, self.s1, self.s2, self.s3 = [World(i) for i in range(4)]
        self._succ = {
            self.s0: {self.s1, self.s2},
            self.s1: {self.s3},
            self.s2: {self.s3},
            self.s3: set(),
        }
    def accessibility(self, w, modality, agent=None):
        if modality == "X":
            return self._succ.get(w, set())
        return set()

Epistemic pattern

class Epistemic(Model):
    def __init__(self):
        self.s = [World(i) for i in range(3)]
        self._K = {
            "alice": {self.s[0]: {self.s[0], self.s[1]},
                      self.s[1]: {self.s[0], self.s[1]},
                      self.s[2]: {self.s[2]}},
            "bob":   {self.s[0]: {self.s[0]},
                      self.s[1]: {self.s[1], self.s[2]},
                      self.s[2]: {self.s[1], self.s[2]}},
        }
    def accessibility(self, w, modality, agent=None):
        if modality == "K" and agent:
            return self._K[agent].get(w, set())
        return set()

Probabilistic pattern

class Probabilistic(Model):
    def __init__(self):
        self.s_rain, self.s_sun = World(0), World(1)
        self._prob = {
            self.s_rain: {self.s_rain: 0.3, self.s_sun: 0.7},
        }
    def probability(self, world, event):
        dist = self._prob.get(world)
        if dist is None:
            return 0.0
        return sum(p for w, p in dist.items() if w in event)

The event argument is the set of worlds satisfying the formula whose probability is being computed. The engine supplies this set automatically.

Dynamic-logic pattern

class ActionModel(Model):
    def __init__(self):
        self.s0, self.s1, self.s2 = World(0), World(1), World(2)
        self._actions = {
            ("enter_order", self.s0): {self.s1},
            ("enter_order", self.s1): {self.s2},
            ("enter_order", self.s2): set(),
        }
    def action_successors(self, w, action_name):
        return set(self._actions.get((action_name, w), set()))

Description-logic pattern

class DLModel(Model):
    def __init__(self):
        self.w = World(0)
        self._concepts = {
            "Doctor":  {"alice", "bob"},
            "Surgeon": {"alice"},
            "Patient": {"p1", "p2"},
        }
        self._roles = {
            "treats": {("alice", "p1"), ("bob", "p2")},
        }
    def concept_extension(self, w, concept):
        return set(self._concepts.get(concept, set()))
    def role_extension(self, w, role):
        return set(self._roles.get(role, set()))
    def domain(self):
        return {"alice", "bob", "p1", "p2"}

Fuzzy pattern

class FuzzyModel(Model):
    def __init__(self):
        self.w = World(0)
        self._grades = {
            ("temp", ()): 0.85,
            ("risk", ("u1",)): 0.72,
        }
    def fuzzy_valuation(self, w, predicate, args):
        return self._grades.get((predicate, tuple(args)), 0.0)

10 Classical logic

phi = parser.parse_string("forall x. (P(x) -> Q(x))")
phi = parser.parse_string("exists x. (P(x) & Q(x))")
phi = parser.parse_string("x + y <= 10")
phi = parser.parse_string("balance >= 0 & balance < limit")

Quantifiers range over model.domain(). If the domain is empty, forall is vacuously true and exists is vacuously false.

11 Modal and epistemic logic

phi = parser.parse_string("[](p -> q) -> ([]p -> []q)")   # K
phi = parser.parse_string("[]p -> p")                     # T
phi = parser.parse_string("[]p -> [][]p")                 # 4
phi = parser.parse_string("<>p -> []<>p")                 # 5

phi = parser.parse_string("K_alice(p)")
phi = parser.parse_string("B_alice(p)")
phi = parser.parse_string("CommonKnows([alice, bob], safe)")

The truth of the modal axioms depends on the frame conditions of model.accessibility. The engine does not enforce frame conditions — it evaluates whatever relation the model provides.

• For knowledge, use an equivalence relation (S5).
• For belief, use a serial relation.
• For common knowledge, provide separate K_<agent> relations.

12 Deontic logic

phi = parser.parse_string("O(report)")
phi = parser.parse_string("P(skip)")
phi = parser.parse_string("Forb(falsify)")
phi = parser.parse_string("O(do(u, op) -> P(do(u, op)))")

O(φ) holds at w if φ holds at every deontically accessible world. P(φ) holds if φ holds at some. Forb(φ) is O(~φ). For the D axiom O(φ) -> P(φ), the relation must be serial.

Access control example

phi = parser.parse_string(
    "Forb(prescribe(u, m) & dispense(u, m))")
# Separation of duty: no user may both prescribe and dispense

13 Temporal logic

phi = parser.parse_string("G(safe)")
phi = parser.parse_string("F(done)")
phi = parser.parse_string("X(next_state)")
phi = parser.parse_string("p U q")
phi = parser.parse_string("G(p -> F q)")
phi = parser.parse_string("G_[0,5](request -> F_[0,3] response)")

Semantics

Temporal formulas are evaluated over paths. A path is a sequence of worlds reachable via the temporal accessibility relation. The model can designate a current path via current_path(w). If no path is designated, the engine treats LTL operators as universally quantified over all paths.

Until and Release

φ U ψ holds on a path starting at position i if:

• ψ holds at some position j ≥ i, and
• φ holds at every position from i to j - 1.

φ R ψ (release) holds if:

• φ holds at some position j ≥ i and ψ holds at every position from i to j, or
• ψ holds at every position from i to the end of the path.

Path quantifiers

A φ holds at w if every path starting at w satisfies φ. E φ holds if some path does.

Practical guidance

• For safety: G(~bad).
• For liveness: G(request -> F response).
• For bounded response: G_[0,N](request -> F_[0,M] response).
• For universal guarantees: A. For existence: E.

14 Dynamic logic

phi = parser.parse_string("[enter_order](order_entered)")
phi = parser.parse_string("<withdraw> balance >= 0")
phi = parser.parse_string("[(a; b)*](~(balance < 0))")
phi = parser.parse_string("<has_permission?; perform_action> success")

[α]φ holds at w if every execution of α starting at w terminates in a state where φ holds. <α>φ holds if some execution does.

Only atomic actions need to be provided by the model via action_successors. Complex actions are interpreted by the engine using the atomic transitions.

15 Description logic

phi = parser.parse_string(
    "SomeConcept(treats, ConceptApplication('Patient', p1))")
phi = parser.parse_string(
    "AndConcept(ConceptApplication('Doctor', alice), "
    "ConceptApplication('Surgeon', alice))")
phi = parser.parse_string(
    "AtLeastConcept(2, authored, ConceptApplication('Paper', p1))")

Concept expressions are interpreted as sets of individuals at each world; roles as sets of pairs. Concept assertions use x : C; role assertions use R(x, y).

16 Probabilistic logic

phi = parser.parse_string("P_>=0.7(rain)")
phi = parser.parse_string("P_>0.5(heads)")
phi = parser.parse_string("P_<=0.1(failure)")
phi = parser.parse_string("P_>=0.95(G(request -> F response))")

P_>=r(φ) holds at w if the probability measure Pr_w assigns at least r to the set of worlds satisfying φ. The engine computes the event set and asks the model for its probability via model.probability(w, event).

17 Non-monotonic reasoning

phi = parser.parse_string("bird => flies")
phi = parser.parse_string("penguin => ~flies")
phi = parser.parse_string("Ab_penguin")

φ => ψ holds at w if, in every ≺-minimal world where φ holds, ψ also holds. This implements Reiter's default logic with a preference-based selection of “most normal” worlds.

Model defaults by making normal cases preferred over exceptional cases in model.preference.

18 Preference and optimisation

phi = parser.parse_string("outcome_a ≺ outcome_b")
phi = parser.parse_string("Opt(minimize(cost))")

φ ≺ ψ holds at w if every world satisfying φ is preferred to every world satisfying ψ at w. Opt(φ) holds if some φ-world is ≺-minimal.

Use preference for goal constraints. Combine with temporal operators for “eventually reach an optimal state”; combine with deontic logic for “preferred but not obligatory” behaviours.

19 Fuzzy logic

phi = parser.parse_string("f_and(high_fever(p), cough(p), \"G\")")
phi = parser.parse_string("f_or(high_risk(u), flagged(u), \"L\")")
phi = parser.parse_string("f_not(normal_temp, \"G\")")
phi = parser.parse_string("T_>=0.8(risk_level(u))")

T-norms

Getting continuous grades

from unilog.engine.solvers import FuzzySolver
from unilog.parser import UniLangParser

phi = UniLangParser().parse_string("f_and(high_risk(u1), flagged(u1), \"G\")")
grade = FuzzySolver().grade(phi, model, World(0), None)
print(grade)   # e.g., 0.72

20 SMT-based verification

For bounded verification, UniLog formulas translate into SMT-LIB and check with a solver such as Z3. The translation creates one boolean copy of each atom per state index and unrolls modal and temporal operators up to a fixed horizon.

Encoding

from unilog.parser import UniLangParser
from unilog.engine.adapters.smt import SMTSolver

phi = UniLangParser().parse_string("G(p -> F q)")

encoder = SMTSolver(horizon=3)
smt2 = encoder.encode(phi, world_names=["w0", "w1", "w2", "w3"])
print(smt2)

Solving with Z3

result, smt2 = encoder.solve_with_z3(phi, ["w0", "w1", "w2", "w3"])
print(result)   # sat, unsat, or unknown

Custom successors and domain

encoder = SMTSolver(
    horizon=3,
    domain=["alice", "bob", "carol"],
    successors={
        ("K", 0): [1],
        ("K", 1): [2],
        ("K", 2): [3],
        ("K", 3): [],
    })

Supported fragment

• Quantifier-free first-order formulas with equality
• Linear integer and real arithmetic
• Modal operators □ and ◇
• Temporal operators X, G, F, U, R (bounded)
• Probabilistic operators P_>=r(φ)
• Quantifiers (expanded over a finite domain)

Operators outside this fragment (fuzzy, common knowledge) are abstracted as fresh booleans. Sound for many queries; may lose precision.

Workflow

1. Write the constraint in UniLang.
2. Define a small model with the relevant worlds and relations.
3. Encode with SMTSolver, supplying the horizon and optionally the transition relation and domain.
4. Solve with Z3 or export the SMT-LIB for another solver.
5. Interpret the result: sat means satisfiable, unsat means not, and a model can be extracted from Z3.

21 COH/CZOA constraint authoring

The four constraint types

Authoring workflow

from unilog.parser import UniLangParser

class Constraint:
    def __init__(self, name, kind, formula_str):
        self.name = name
        self.kind = kind
        self.formula = UniLangParser().parse_string(formula_str)

zone_containment = Constraint(
    name="ZoneContainment",
    kind="identity",
    formula_str="G(forall u (inZone(u, z) -> inZone(u, parent(z))))")

lab_alert = Constraint(
    name="CriticalLabAlert",
    kind="trigger",
    formula_str="G(labResult(p, r) & critical(r) -> X(alertPhysician(p)))")

mortality_goal = Constraint(
    name="MinimizeMortality",
    kind="goal",
    formula_str="forall r1, r2 (mortalityRate(r1) ≺ mortalityRate(r2) "
                "<-> r1 < r2)")

sod = Constraint(
    name="SeparationOfDuty",
    kind="access",
    formula_str="Forb(prescribe(u, m) & dispense(u, m))")

Integration with CZOI

class AccessController:
    def __init__(self, model):
        self.model = model
        self.engine = InferenceEngine.get_instance()
        self.constraints = []

    def add(self, constraint):
        self.constraints.append(constraint)

    def decide(self, world):
        for constraint in self.constraints:
            if not self.engine.evaluate(constraint.formula, self.model, world):
                return False
        return True

Best practices

• One constraint per logical unit. Group related constraints but keep them separate for incremental verification.
• Name descriptively. CriticalLabAlert is better than trigger_1.
• Document intended semantics. A comment on when the constraint fires saves time later.
• Test both directions. A constraint that is trivially true is often wrong.

22 Real-world scenarios

Healthcare — sepsis alert

phi = parser.parse_string(
    "G(sepsisRisk(p) >= 0.8 -> "
    "   F_[0,1](assessed(p)) & F_[0,3](antibiotics(p)))")

Finance — insider trading detection

phi = parser.parse_string(
    "G((K_employee(material_info(s))) -> Forb(trade(employee, s))))")

Smart city — traffic incident response

phi = parser.parse_string(
    "G(incident_detected(z) -> "
    "   [access_zones] F_[0,2](reroute(z)))")

University — academic probation

phi = parser.parse_string(
    "(gpa(s) < 2.0 & ~exception(s)) => probation(s)")

Supply chain — cold chain monitoring

phi = parser.parse_string(
    "G(f_and(T_>=0.9(temperature_risk(shipment)), "
    "         T_>=0.8(duration_risk(shipment)), \"G\") "
    "   -> O(flag_for_inspection(shipment)))")

Cross-domain integration

phi = parser.parse_string(
    "P_>=0.9(G(K_physician(critical(p, r)) -> "
    "          O(X(alert(p))))))")

Read: “with probability at least 0.9, whenever the physician knows the result is critical for patient p, alerting p in the next state is obligatory.” Such formulas are the primary use case for UniLog — awkward in any single traditional logic and natural here.

23 Extending the toolkit

Custom solvers

from unilog.engine.adapters.base import Solver
from unilog import ast

class MySolver(Solver):
    name = "my_module"

    def supports(self, formula):
        return isinstance(formula, ast.Atom) and formula.name.startswith("my_")

    def evaluate(self, formula, model, world, assignment):
        return model.valuation(world, formula.name, tuple(formula.args))

engine = InferenceEngine.get_instance()
engine.register_solver(MySolver())

Solvers are inserted at the front of the dispatch list, so your solver takes precedence over built-in solvers that might also support the formula.

Custom AST nodes

from dataclasses import dataclass
from unilog.ast import Formula

@dataclass(frozen=True)
class MyCustomFormula(Formula):
    sub: Formula
    parameter: str = "default"

Extend the parser to recognise the syntax, and add a solver to evaluate it.

Custom model structures

class MyModel(Model):
    def my_custom_relation(self, w):
        return self._my_relation.get(w, set())

Extending the SMT encoder

class MyEncoder(SMTSolver):
    def _enc(self, f, i):
        if isinstance(f, MyCustomFormula):
            return f"(my_op {self._enc(f.sub, i)} {f.parameter})"
        return super()._enc(f, i)

24 Testing your constraints

Positive and negative tests

Every constraint should have at least one test where it holds and one where it fails. This guards against constraints that are vacuously true or trivially false.

def test_alert_holds():
    model = HospitalWithAlert()
    phi = parser.parse_string("G(critical(p1) -> X(alerted(p1)))")
    assert engine.evaluate(phi, model, model.s0)

def test_alert_fails_without_alert():
    model = HospitalWithoutAlert()
    phi = parser.parse_string("G(critical(p1) -> X(alerted(p1)))")
    assert not engine.evaluate(phi, model, model.s0)

Property-based testing

from hypothesis import given, strategies as st

@given(threshold=st.floats(min_value=0.0, max_value=1.0))
def test_probability_threshold_monotone(threshold):
    r = threshold
    s = threshold / 2
    phi_r = parser.parse_string(f"P_>={r}(rain)")
    phi_s = parser.parse_string(f"P_>={s}(rain)")
    m = UniformRainModel()
    if engine.evaluate(phi_r, m, m.w):
        assert engine.evaluate(phi_s, m, m.w)

Meta-theoretic tests

def test_conservativity():
    core_model = CoreModel()
    extended_model = ExtendedModel()  # adds probability, preference, ...
    phi = parser.parse_string("p & q")   # core formula
    assert engine.evaluate(phi, core_model, core_model.w) == \
           engine.evaluate(phi, extended_model, extended_model.w)

25 Troubleshooting & FAQ

Parser errors

Unexpected character. Usually curly quotes, Unicode whitespace, or an unsupported operator. Use straight quotes ("), ASCII whitespace, and operators from §5.

Unbalanced parentheses. Nested modalities are the usual suspects: G(p -> F q) needs two closing parentheses.

Trailing tokens. Usually a missing operator between subformulas. p q should be p & q or p -> q.

Evaluation errors

Missing model method. The Model base class requires all seven methods even if your formulas do not use them. Return None, set(), 0.0, or False as appropriate.

Formula returns unexpected False. Check, in order:

1. Is valuation returning the right values at the right worlds?
2. Is the accessibility relation correct for the modality? []φ uses modality="K" by default.
3. For temporal formulas, is current_path returning the right path?
4. For quantifiers, is domain() returning the expected set?

SMT errors

Z3 not installed. Only solve_with_z3 requires it. encode works without Z3.

Z3 returns unknown. The fragment used a feature Z3 cannot decide. Check the logic string passed to SMTSolver.

Frequently asked questions

Can I use UniLog without a parser?
Yes. Construct AST nodes directly:

from unilog import ast
phi = ast.Implies(ast.Atom("p"), ast.Atom("q"))

Can I combine modal and temporal operators in one formula?
Yes. G([]p) is valid. Modal operators use the modal accessibility; temporal operators use the temporal one.

What does “fibred” mean in practice?
Each module extends the core conservatively. Adding a module does not change the truth value of formulas that do not use the module's operators.

How do I know which solver handles my formula?
The engine tries solvers in registration order and uses the first one that returns True from supports. To inspect the order: InferenceEngine.get_instance().solvers.

Can I override a built-in solver?
Yes. engine.register_solver(MySolver()) inserts at the front of the list.

Are formulas cached?
Not currently. Cache the AST yourself if you evaluate the same formula many times:

from functools import lru_cache

@lru_cache(maxsize=1024)
def parse_cached(src):
    return UniLangParser().parse_string(src)

How large can models be?
Up to a few thousand worlds for purely propositional reasoning. Modal and temporal reasoning is exponential in the branching factor and path length. For larger models, use the SMT encoder with a bounded horizon.

Can I run UniLog without ANTLR?
Yes. The runtime parser is hand-written and does not depend on ANTLR. The UniLang.g4 grammar is provided for compatibility.

26 Glossary

Accessibility relation. A binary relation on worlds determining which are reachable via a given modality.

Action. In dynamic logic, a program built from atomic actions using sequencing, choice, iteration, and tests.

AST. Abstract syntax tree — the internal representation of a parsed formula.

Common knowledge. A fact known by all agents, known to be known by all agents, and so on. Modelled as the reflexive-transitive closure of the union of the agents' epistemic relations.

Conservativity. Adding a module does not change the truth value of formulas that do not use the module's operators.

CTL. Computation Tree Logic — branching-time temporal logic with universal (A) and existential (E) path quantifiers.

CZOA. Constrained Zone-Object Architecture — enterprise-oriented extension of COH.

COH. Constrained Object Hierarchies — the base framework.

Deontic logic. Logic of obligation, permission, and prohibition.

Description logic (DL). A decidable fragment of FOL designed for ontological reasoning.

Epistemic logic. Logic of knowledge and belief.

Fibring. A systematic method for combining logics by fusing their semantic structures (Gabbay).

Fuzzy logic. A logic with continuous truth values in [0, 1].

Horizon. Maximum depth to which modal/temporal operators are unrolled in the SMT encoding.

Kripke frame. A set of worlds with a family of accessibility relations.

LTL. Linear Temporal Logic — a temporal logic over a single execution path.

Modality. A modal operator such as □ or ◇, or its epistemic/deontic analogue.

PDL. Propositional Dynamic Logic.

Preference relation. A binary relation on worlds ordering them by desirability or normality.

Satisfaction relation. M, w ⊨ φ — formula φ holds at world w in model M.

SMT. Satisfiability Modulo Theories.

SMT-LIB. Standard input format for SMT solvers.

Solver. A module in the engine that evaluates one family of operators.

T-norm. A function [0,1] × [0,1] → [0,1] generalising conjunction to fuzzy logic. Standard t-norms: Gödel, Łukasiewicz, Product.

UniLang. The concrete syntax of UniLog.

World. A point at which a formula is evaluated.

Z3. A state-of-the-art SMT solver from Microsoft Research.