Bimodal Z3 Semantics

[benbrastmckie]

The bimodal semantics takes worlds to be partial functions from the integers to world states (bitvectors).
In order to quantify over worlds, I include a world_function which is variously constrained to enumerate the worlds so that I can quantify over these number (names of worlds) in the semantic clauses in bimodal/operators.py.

The current version of the theory_lib/bimodal/semantic.py sets up the following primitives:

def define_sorts(self):
    """Define the Z3 sorts used in the bimodal logic model.

    Create three sorts:
    - WorldStateSort: BitVecSort for representing world states as bitvectors
    - TimeSort: IntSort for representing time points
    - WorldIdSort: IntSort for mapping world IDs to world arrays
    """            
    self.WorldStateSort = z3.BitVecSort(self.N)
    self.TimeSort = z3.IntSort()
    self.WorldIdSort = z3.IntSort()


def define_primitives(self):
    """Define the Z3 primitive functions and relations used in the bimodal logic model.
    
    In bimodal logic we distinguish between:
    - World States: Instantaneous configurations of the system (e.g., {a, b, c})
    - World Histories: Temporally extended sequences of states that follow lawful transitions
    
    This method initializes:
    - task: A binary relation between world states representing transitions between states
    - world_function: A mapping from world IDs to world histories (arrays mapping time -> world state)
    - truth_condition: A function assigning truth values to atomic propositions at instantaneous world states
    - main_world: The primary world history used for evaluation (world_function applied to ID 0)
    - main_time: The time point at which sentences are evaluated
    - main_point: Dictionary containing the main world history and evaluation time
    - is_world: A boolean function indicating whether a world_id maps to a valid world history
    """
    # Define the task relation between world states
    self.task = z3.Function(
        "Task",
        self.WorldStateSort,
        self.WorldStateSort,
        z3.BoolSort()
    )

    # Mapping from world IDs to world histories (arrays from time to state)
    self.world_function = z3.Function(
        'world_function', 
        self.WorldIdSort,  # Input: world ID 
        z3.ArraySort(self.TimeSort, self.WorldStateSort)  # Output: world history
    )

    # Function to determine if a world_id maps to a valid world history
    self.is_world = z3.Function(
        'is_world',
        self.WorldIdSort,  # Input: world ID
        z3.BoolSort()      # Output: whether it's a valid world history
    )

    # Set a reasonable limit on world IDs for efficiency
    self.max_world_id = self.M * (2 ** (self.M * self.N))  # Number of possible world histories
    
    # Truth condition for atomic propositions at world states
    self.truth_condition = z3.Function(
        "truth_condition",
        self.WorldStateSort,
        syntactic.AtomSort,
        z3.BoolSort()
    )

    # Define interval tracking functions
    self.world_interval_start = z3.Function(
        'world_interval_start',
        self.WorldIdSort,  # World ID
        self.TimeSort      # Start time of interval
    )
    
    self.world_interval_end = z3.Function(
        'world_interval_end',
        self.WorldIdSort,  # World ID
        self.TimeSort      # End time of interval
    )
    
    # Dictionary to store world time intervals after extraction
    self.world_time_intervals = {}
    
    # Main point of evaluation includes a world ID and time
    self.main_world = 0             # Store world ID, not array reference
    self.main_time = z3.IntVal(0)   # Fix the main time to 0 
    self.main_point = {
        "world": self.main_world,  
        "time": self.main_time,
    } 

This works, but assumes that time is bounded above and below where the performance is not great.
I have nevertheless gotten the examples in bimodal/examples.py to work, though with some inconsistencies where there seems to be poor isolation between examples (running two examples can give different result from running just one).
I have tried various things to isolate examples but without success.

Separately, I have begun developing a version of the semantics which does not assume as much about time:

def define_sorts(self):
    """Define the Z3 sorts used in the bimodal logic model.

    Create three sorts:
    - WorldStateSort: BitVecSort for representing world states as bitvectors
    - TimeSort: IntSort for representing time points
    - WorldIdSort: IntSort for mapping world IDs to world arrays
    """            
    self.WorldStateSort = z3.BitVecSort(self.N)
    self.TimeSort = z3.IntSort()
    self.WorldIdSort = z3.IntSort()


def define_primitives(self):
    """Define the Z3 primitive functions and relations used in the bimodal logic model.
    
    In bimodal logic we distinguish between:
    - World States: Instantaneous configurations of the system (e.g., {a, b, c})
    - World Histories: Temporally extended sequences of states that follow lawful transitions
    
    This method initializes:
    - task: A binary relation between world states representing transitions between states
    - world_function: A mapping from world IDs to world histories (arrays mapping time -> world state)
    - truth_condition: A function assigning truth values to atomic propositions at instantaneous world states
    - main_world: The primary world history used for evaluation (world_function applied to ID 0)
    - main_time: The time point at which sentences are evaluated
    - main_point: Dictionary containing the main world history and evaluation time
    - is_world: A boolean function indicating whether a world_id maps to a valid world history
    - defined_at_time: A function indicating whether a world is defined at a specific time
    """
    
    # Define the task relation between world states
    self.task = z3.Function(
        "Task",
        self.WorldStateSort,
        self.WorldStateSort,
        z3.BoolSort()
    )

    # Mapping from world IDs to world histories (arrays from time to state)
    self.world_function = z3.Function(
        'world_function', 
        self.WorldIdSort,  # Input: world ID 
        z3.ArraySort(self.TimeSort, self.WorldStateSort)  # Output: world history
    )
    
    # Function to determine if a world_id maps to a valid world history
    self.is_world = z3.Function(
        'is_world',
        self.WorldIdSort,  # Input: world ID
        z3.BoolSort()      # Output: whether it's a valid world history
    )
    
    # Function to determine if a world is defined at a specific time
    self.defined_at_time = z3.Function(
        'defined_at_time',
        self.WorldIdSort,  # Input: world ID
        self.TimeSort,     # Input: time
        z3.BoolSort()      # Output: whether world is defined at time
    )
    
    # Remove explicit maximum world ID limit
    # We'll rely on Z3's natural minimality instead
    
    # Truth condition for atomic propositions at world states
    self.truth_condition = z3.Function(
        "truth_condition",
        self.WorldStateSort,
        syntactic.AtomSort,
        z3.BoolSort()
    )
    
    # Dictionary to store world time intervals after extraction
    self.world_time_intervals = {}
    
    # Main point of evaluation with world ID and time
    self.main_world = z3.IntVal(0)
    self.main_time = z3.IntVal(0)
    self.main_point = {
        "world": self.main_world,
        "time": self.main_time,
    }

This has proven to be faster in some ways, but much less consistent in its outputs, at least so far.
Here are the frame constraints that I am struggling to optimize to get the right logical consequences to go through without sinking Z3:

def build_frame_constraints(self):
    """Build the core frame constraints for the bimodal logic model.
    
    These constraints define the fundamental structure of legal models
    with a focus on logical correctness and generality.
    
    Returns:
        list: A list of Z3 constraints that define the frame conditions
    """
    constraints = []
    
    # 1. Main point exists - world 0 at time 0 is defined
    main_point_constraint = z3.And(
        self.is_world(self.main_world),
        self.defined_at_time(self.main_world, self.main_time)
    )
    
    # 2. World enumeration starts at 0 and is continuous
    enumerate_world = z3.Int('enumerate_world')
    enumerate_worlds = z3.ForAll(
        [enumerate_world],
        z3.Implies(
            self.is_world(enumerate_world),
            enumerate_world >= 0
        )
    )
    
    # 3. Worlds form a convex ordering (no gaps)
    convex_world = z3.Int('convex_world')
    convex_world_ordering = z3.ForAll(
        [convex_world],
        z3.Implies(
            z3.And(self.is_world(convex_world), convex_world > 0),
            self.is_world(convex_world - 1)
        )
    )
    
    # 4. All worlds have at least one time point
    world_has_time = z3.Int('world_has_time')
    time_existence = z3.Int('time_existence')
    worlds_have_times = z3.ForAll(
        [world_has_time],
        z3.Implies(
            self.is_world(world_has_time),
            z3.Exists(
                [time_existence],
                self.defined_at_time(world_has_time, time_existence)
            )
        )
    )

    # 5. Time intervals are coherent (no gaps)
    coherence_world = z3.Int('coherence_world')
    coherence_time = z3.Int('coherence_time') 
    future_time = z3.Int('future_time')
    between_time = z3.Int('between_time')
    coherence_constraint = z3.ForAll(
        [coherence_world, coherence_time, future_time],
        z3.Implies(
            z3.And(
                self.is_world(coherence_world),
                self.defined_at_time(coherence_world, coherence_time),
                self.defined_at_time(coherence_world, future_time),
                coherence_time < future_time
            ),
            # All times between must also be defined
            z3.ForAll(
                [between_time],
                z3.Implies(
                    z3.And(coherence_time < between_time, between_time < future_time),
                    self.defined_at_time(coherence_world, between_time)
                )
            )
        )
    )
    
    # 6. Each sentence letter has a definite truth value at each state
    world_state = z3.BitVec('world_state', self.N)
    sentence_letter = z3.Const('atom_interpretation', syntactic.AtomSort)
    classical_truth = z3.ForAll(
        [world_state, sentence_letter],
        z3.Or(
            self.truth_condition(world_state, sentence_letter),
            z3.Not(self.truth_condition(world_state, sentence_letter))
        )
    )
    
    # 7. Worlds are lawful (consecutive states follow task relation)
    lawful_world = z3.Int('lawful_world_id')
    lawful_time = z3.Int('lawful_time')
    worlds_are_lawful = z3.ForAll(
        [lawful_world, lawful_time],
        z3.Implies(
            z3.And(
                self.is_world(lawful_world),
                self.defined_at_time(lawful_world, lawful_time),
                self.defined_at_time(lawful_world, lawful_time + 1)
            ),
            self.task(
                z3.Select(self.world_function(lawful_world), lawful_time),
                z3.Select(self.world_function(lawful_world), lawful_time + 1)
            )
        )
    )

    # 8. Every valid world is unique - simple unified approach
    world_one = z3.Int('world_one')
    world_two = z3.Int('world_two')
    diff_time = z3.Int('diff_time')
    
    world_uniqueness = z3.ForAll(
        [world_one, world_two],
        z3.Implies(
            z3.And(
                self.is_world(world_one),
                self.is_world(world_two),
                world_one != world_two  # Different world IDs
            ),
            z3.Or(
                # CASE 1: Worlds differ in state at a shared time point
                z3.Exists([diff_time],
                    z3.And(
                        self.defined_at_time(world_one, diff_time),
                        self.defined_at_time(world_two, diff_time),
                        z3.Select(self.world_function(world_one), diff_time) !=
                        z3.Select(self.world_function(world_two), diff_time)
                    )
                ),
                
                # CASE 2: Worlds differ in temporal domain
                z3.Exists([diff_time],
                    z3.Or(
                        z3.And(
                            self.defined_at_time(world_one, diff_time),
                            z3.Not(self.defined_at_time(world_two, diff_time))
                        ),
                        z3.And(
                            z3.Not(self.defined_at_time(world_one, diff_time)),
                            self.defined_at_time(world_two, diff_time)
                        )
                    )
                )
            )
        )
    )

    # 9. All valid time-shifted worlds exist (abundance constraint) - simplified
    source_world = z3.Int('abundance_source_world')
    source_time = z3.Int('abundance_source_time')
    target_world = z3.Int('abundance_target_world')
    
    # Forward abundance (simplified)
    forward_abundance = z3.ForAll(
        [source_world, source_time],
        z3.Implies(
            z3.And(
                # When source world and time are defined
                self.is_world(source_world),
                self.defined_at_time(source_world, source_time),
                # And the next time is also defined
                self.defined_at_time(source_world, source_time + 1)
            ),
            # Then a witness world exists with that future state at time 0
            z3.Exists([target_world],
                z3.And(
                    self.is_world(target_world),
                    self.defined_at_time(target_world, 0),
                    z3.Select(self.world_function(target_world), 0) ==
                    z3.Select(self.world_function(source_world), source_time + 1)
                )
            )
        )
    )
    
    # Backward abundance (simplified)
    backward_abundance = z3.ForAll(
        [source_world, source_time],
        z3.Implies(
            z3.And(
                # When source world and time are defined
                self.is_world(source_world),
                self.defined_at_time(source_world, source_time),
                # And the previous time is also defined
                self.defined_at_time(source_world, source_time - 1)
            ),
            # Then a witness world exists with that past state at time 0
            z3.Exists([target_world],
                z3.And(
                    self.is_world(target_world),
                    self.defined_at_time(target_world, 0),
                    z3.Select(self.world_function(target_world), 0) ==
                    z3.Select(self.world_function(source_world), source_time - 1)
                )
            )
        )
    )
    
    # 10. Task relation constraint: tasks match actual world transitions
    some_state = z3.BitVec('task_restrict_some_state', self.N)
    next_state = z3.BitVec('task_restrict_next_state', self.N)
    task_world = z3.Int('task_world')
    task_time = z3.Int('task_time')

    task_restriction = z3.ForAll(
        [some_state, next_state],
        z3.Implies(
            # When task relation holds between states
            self.task(some_state, next_state),
            # Those states must appear in sequence in some world history
            z3.Exists([task_world, task_time],
                z3.And(
                    # The witness world must be a valid world
                    self.is_world(task_world),
                    # Both time points must be defined
                    self.defined_at_time(task_world, task_time),
                    self.defined_at_time(task_world, task_time + 1),
                    # The world has the states in sequence
                    some_state == z3.Select(self.world_function(task_world), task_time),
                    next_state == z3.Select(self.world_function(task_world), task_time + 1)
                )
            )
        )
    )

I'm curious if there are any other broad strategies or approaches that I might look into which could help.

[philzook58]

One thing to maybe consider is trying Vampire. You've got some quantification in there which vampire may be better at. A caveat is that vampire may be less good at integer reasoning? I would not guarantee this will help, but if you're really stumped it may be worth a shot.

My library uses the z3py ast and prints it out to vampire if you have a binary on your system. My code is known to be a little finicky though. It replicates the same interface as z3.Solver. I do not currently parse countermodels. You need a vampire binary install on your system. https://github.com/vprover/vampire
You may also try just s.sexpr() dumping to smtlib from your current solver, since vampire accepts smtlib

https://github.com/philzook58/knuckledragger/blob/9a46c0f31380a948c6a27807b176ca1309484f49/kdrag/solvers/__init__.py#L480

from kdrag.solvers import VampireSolver
import z3
T = z3.DeclareSort("T")
x,y,z = z3.Consts("x y z", T)
s = VampireSolver()
s.add(x != y)
s.check()

I was trying some related kripke model encodings here
https://www.philipzucker.com/shallow_logic_knuckle/
https://github.com/philzook58/knuckledragger/blob/main/kdrag/theories/logic/intuitionistic.py
https://github.com/philzook58/knuckledragger/blob/main/kdrag/theories/logic/temporal.py
I was not really expecting it to scale fully automatically, but I was fine with the idea of proving things interactively. You might also find the Logikey line of work interesting https://arxiv.org/abs/2502.19311

You may want to bounded model check it by expanding out all your quantifiers to a finite number of time steps manually by manipulating the z3 ast if that makes sense for you. Or maybe consider making your worlds and time bitvectors as well.

There's also some interesting stuff in https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/ that might be useful for built in axiomatization of accessibility relation properties. I haven't tried much.

If you really need induction-y proofs, SPACER https://microsoft.github.io/z3guide/docs/fixedpoints/engineforpdr might be interesting. It's a whole other rabbit hole.

You may get different performance if it is acceptable to axiomatize your worlds and time as uninterpreted DeclareSort instead of Int, which is powerful but carries it's own baggage that maybe isn't that relevant.