Research and develop semantic theories using ModelChecker with Z3 SMT solver. Define operators, adjust frame constraints, create examples, run tests, and report findings. Invoke with /mc or when working with model-checker, semantic theories, or Z3 constraints.
Standardmäßig ist der Prompt ausgewählt, der zuerst die Quelle prüft. Sie können zu einem direkten Befehl wechseln oder eine lokale Kopie herunterladen.
Quelldateien prüfen
Lesen Sie SKILL.md und alle von SkillsMP angezeigten Begleitdateien, bevor Sie sich für eine Installation entscheiden.
Mit Codex oder Claude installieren Kopieren Sie diesen Prompt, fügen Sie ihn in Codex, Claude oder einen anderen Assistant ein und lassen Sie die Skill-Seite prüfen und installieren.
Ein direkter Befehl überspringt den Prüf-Prompt. Prüfen Sie die Quelle, bevor Sie ihn ausführen.
Research and develop semantic theories using ModelChecker with Z3 SMT solver. Define operators, adjust frame constraints, create examples, run tests, and report findings. Invoke with /mc or when working with model-checker, semantic theories, or Z3 constraints.
# All tests
PYTHONPATH=Code/src pytest Code/tests/ -v
# Specific theory
PYTHONPATH=Code/src pytest Code/src/model_checker/theory_lib/logos/tests/ -v
# With coverage
PYTHONPATH=Code/src pytest --cov=model_checker --cov-report=term-missing
Operator Definition Workflow
When to Use
Use /mc operator when:
Adding a new logical operator
Modifying existing operator semantics
Implementing operator for a new subtheory
Theory Structure
Each theory follows this pattern:
theory_lib/{theory}/
├── __init__.py # Public API
├── semantic.py # Core semantic framework
├── operators.py # Operator registry
├── examples.py # Test cases
└── tests/
├── unit/ # Unit tests
└── integration/ # Integration tests
Operator Class Template
from model_checker.syntactic import Operator
classMyOperator(Operator):
"""
Operator implementing {description}.
Syntax: A \\myop B
"""
name = "\\myop"# LaTeX-style name
arity = 2# Number of argumentsdeftrue_at(self, left, right, eval_point):
"""
Truth conditions: when is 'A \\myop B' true at eval_point?
Args:
left: Left argument sentence
right: Right argument sentence
eval_point: Dict with 'world' key containing Z3 BitVec
Returns:
Z3 constraint for truth condition
"""
world = eval_point["world"]
# Example: conjunction semanticsreturn z3.And(
self.semantics.true_at(left, eval_point),
self.semantics.true_at(right, eval_point)
)
deffalse_at(self, left, right, eval_point):
"""
Falsity conditions: when is 'A \\myop B' false at eval_point?
"""
world = eval_point["world"]
# Example: conjunction falsity (either false)return z3.Or(
self.semantics.false_at(left, eval_point),
self.semantics.false_at(right, eval_point)
)
defextended_verify(self, state, left, right, eval_point):
"""
Hyperintensional verification: state verifies 'A \\myop B'.
Args:
state: Z3 BitVec representing a state
left, right: Argument sentences
eval_point: Evaluation point
"""# Example: fusion of verifiers
x, y = z3.BitVecs("ver_x ver_y", self.semantics.N)
return z3.Exists([x, y], z3.And(
self.semantics.extended_verify(x, left, eval_point),
self.semantics.extended_verify(y, right, eval_point),
state == self.semantics.fusion(x, y)
))
defextended_falsify(self, state, left, right, eval_point):
"""
Hyperintensional falsification: state falsifies 'A \\myop B'.
"""# Example: either falsifier sufficesreturn z3.Or(
self.semantics.extended_falsify(state, left, eval_point),
self.semantics.extended_falsify(state, right, eval_point)
)
deffind_verifiers_and_falsifiers(self, left, right, eval_point):
"""
Compute proposition as (verifier_set, falsifier_set).
Used for output display.
"""
left_prop = self.semantics.find_proposition(left, eval_point)
right_prop = self.semantics.find_proposition(right, eval_point)
# Combine based on operator semantics
verifiers = set()
for lv in left_prop[0]:
for rv in right_prop[0]:
verifiers.add(self.semantics.fusion(lv, rv))
falsifiers = left_prop[1] | right_prop[1]
return (verifiers, falsifiers)
Operator Registration
Add to operators.py:
from .my_operator import MyOperator
defload_operators(semantics):
"""Load all operators for this theory."""return [
# ... existing operators ...
MyOperator(semantics),
]
TDD Workflow for Operators
1. Write failing test first:
# tests/unit/test_my_operator.pyimport pytest
from model_checker.builder import BuildExample
classTestMyOperator:
deftest_basic_truth(self):
"""Test basic truth conditions for \\myop."""
example = BuildExample(
premises=['A', 'B'],
conclusions=['A \\myop B'],
settings={'N': 3, 'expectation': False} # Should be theorem
)
result = example.run()
assert result.is_theorem(), "A, B should entail A \\myop B"deftest_countermodel(self):
"""Test that invalid inference has countermodel."""
example = BuildExample(
premises=['A \\myop B'],
conclusions=['A'],
settings={'N': 3, 'expectation': True} # Should find countermodel
)
result = example.run()
assert result.has_countermodel()
from model_checker.semantic import SemanticDefaults
from model_checker.utils import ForAll, Exists
import z3
classMySemantics(SemanticDefaults):
def__init__(self, combined_settings=None, **kwargs):
super().__init__(combined_settings)
# Z3 primitivesself.verify = z3.Function(
"verify",
z3.BitVecSort(self.N),
syntactic.AtomSort,
z3.BoolSort()
)
self.falsify = z3.Function(
"falsify",
z3.BitVecSort(self.N),
syntactic.AtomSort,
z3.BoolSort()
)
self.possible = z3.Function(
"possible",
z3.BitVecSort(self.N),
z3.BoolSort()
)
# Main evaluation pointself.main_world = z3.BitVec("w", self.N)
self.main_point = {"world": self.main_world}
# Build frame constraintsself._build_frame_constraints()
def_build_frame_constraints(self):
"""Define the frame constraints for this semantic theory."""
x, y = z3.BitVecs("frame_x frame_y", self.N)
# Possibility is downward closed under parthood
possibility_downward = ForAll([x, y], z3.Implies(
z3.And(self.possible(y), self.is_part_of(x, y)),
self.possible(x)
))
# Main world is a world
main_is_world = self.is_world(self.main_world)
# Verifiers must be possible
atom = z3.Const("frame_atom", syntactic.AtomSort)
verifier_possible = ForAll([x, atom], z3.Implies(
self.verify(x, atom),
self.possible(x)
))
self.frame_constraints = [
possibility_downward,
main_is_world,
verifier_possible,
]
# Validity conditionsself.premise_behavior = lambda p: self.true_at(p, self.main_point)
self.conclusion_behavior = lambda c: self.false_at(c, self.main_point)
Common Constraint Patterns
Constraint
Z3 Pattern
Universal
ForAll([x], condition(x))
Existential
Exists([x], condition(x))
Parthood
self.is_part_of(x, y) (x <= y in bitvec)
Fusion
self.fusion(x, y) (x | y in bitvec)
Possibility
self.possible(x)
World
self.is_world(x) (maximal possible state)
Example Creation Workflow
When to Use
Use /mc example when:
Creating test cases for operators
Validating logical relationships
Building countermodel demonstrations
Example Naming Convention
{SUBTHEORY}_{TYPE}_{NUMBER}
SUBTHEORY: EXT, MOD, CONST, CF, REL (or theory-specific)
TYPE: CM (countermodel expected), TH (theorem expected)
NUMBER: Sequential number
Example Template
# examples.py# Countermodel example (expect to find model)
EXT_CM_1_premises = ['A']
EXT_CM_1_conclusions = ['B']
EXT_CM_1_settings = {
'N': 3, # State space size (2^N states)'contingent': False, # Force contingent propositions'non_null': True, # Exclude null state verifiers'non_empty': True, # Require non-empty verifier sets'disjoint': False, # Allow verifier/falsifier overlap'max_time': 1, # Solver timeout (seconds)'iterate': 1, # Number of models to find'expectation': True, # True = expect countermodel
}
EXT_CM_1_example = [
EXT_CM_1_premises,
EXT_CM_1_conclusions,
EXT_CM_1_settings,
]
# Theorem example (expect no countermodel)
EXT_TH_1_premises = ['A', '(A \\rightarrow B)']
EXT_TH_1_conclusions = ['B']
EXT_TH_1_settings = {
'N': 3,
'max_time': 1,
'expectation': False, # False = expect theorem (no countermodel)
}
EXT_TH_1_example = [
EXT_TH_1_premises,
EXT_TH_1_conclusions,
EXT_TH_1_settings,
]
# Organize into collections
countermodel_examples = {
"EXT_CM_1": EXT_CM_1_example,
}
theorem_examples = {
"EXT_TH_1": EXT_TH_1_example,
}
# Active examples for testing
example_range = {
**countermodel_examples,
**theorem_examples,
}
Settings Reference
Setting
Type
Default
Description
N
int
16
State space size (2^N possible states)
contingent
bool
True
Force propositions to be contingent
non_empty
bool
True
Verifier/falsifier sets must be non-empty
non_null
bool
True
Exclude null state from verifiers
disjoint
bool
True
Verifiers and falsifiers must be disjoint
max_time
int
10
Solver timeout in seconds
iterate
int/bool
False
Number of models to find (False = 1)
expectation
bool/None
None
True=countermodel, False=theorem, None=unknown
Testing Workflow
When to Use
Use /mc test when:
Running theory tests
Validating examples
Checking test coverage
Test Commands
# All tests
PYTHONPATH=Code/src pytest Code/tests/ -v
# Specific theory
PYTHONPATH=Code/src pytest Code/src/model_checker/theory_lib/logos/tests/ -v
PYTHONPATH=Code/src pytest Code/src/model_checker/theory_lib/exclusion/tests/ -v
PYTHONPATH=Code/src pytest Code/src/model_checker/theory_lib/imposition/tests/ -v
PYTHONPATH=Code/src pytest Code/src/model_checker/theory_lib/bimodal/tests/ -v
# Specific test file
PYTHONPATH=Code/src pytest Code/src/model_checker/theory_lib/logos/tests/unit/test_semantic.py -v
# With coverage
PYTHONPATH=Code/src pytest --cov=model_checker --cov-report=term-missing
# Run single test
PYTHONPATH=Code/src pytest -k "test_name" -v
Test Fixture Pattern
import pytest
from model_checker.theory_lib.logos import get_theory, get_examples
@pytest.fixturedeftheory():
"""Get logos theory instance."""return get_theory()
@pytest.fixturedefexamples():
"""Get example collection."""return get_examples()
classTestOperator:
deftest_truth_conditions(self, theory):
"""Test operator truth conditions."""# ... test code ...deftest_with_examples(self, examples):
"""Test against standard examples."""for name, example in examples.items():
result = example.run()
# Validate based on expectation
Common Test Failures
Error
Cause
Fix
ImportError
PYTHONPATH not set
Add PYTHONPATH=Code/src
z3.Z3Exception
Constraint type mismatch
Check BitVec sizes match
Timeout
State space too large
Reduce N or add constraints
Wrong result
Semantic error
Check operator methods
Reporting Workflow
When to Use
Use /mc report when:
Analyzing countermodel structure
Documenting logical results
Comparing theories
Model Output Interpretation
When a countermodel is found:
=== COUNTERMODEL FOUND ===
World (w): 0b1101 (state 13)
Atoms:
A: verifiers={0b0001, 0b0101}, falsifiers={0b0010}
B: verifiers={0b0100}, falsifiers={0b0001, 0b0011}
Premises satisfied:
A is TRUE at w (verified by 0b0101 which is part of w)
Conclusion falsified:
B is FALSE at w (falsified by 0b0001 which is part of w)
Key interpretation:
World: The evaluation world as a bitvector (maximal possible state)
Verifiers: States that make the proposition true
Falsifiers: States that make the proposition false
Parthood: x is part of y if (x & y) == x (bitvector AND)
Report Template
# Model-Checker Analysis: {Topic}**Date**: {date}
**Theory**: {logos/exclusion/imposition/bimodal}
## Formula Under Test
Premises:
- {premise 1}
- {premise 2}
Conclusion:
- {conclusion}
## Result
{THEOREM / COUNTERMODEL FOUND}
## Analysis
{Explanation of the logical significance}
## Model Details (if countermodel)
{Countermodel structure and interpretation}
## Implications
{What this tells us about the logical system}
Theory Comparison
Run same formula across theories:
# Compare all theories
model-checker examples.py --maximize
# This runs the example against all available theories# and reports which theory finds the smallest countermodel# (or which validates as theorem)
import z3
from model_checker.utils import ForAll, Exists
# BitVector state (N bits)
x = z3.BitVec("x", N)
state = z3.BitVecVal(5, N) # Concrete state 0b101# Parthood: x is part of y
is_part = (x & y) == x
# Fusion: combine states
fusion = x | y
# Quantified constraints
ForAll([x], z3.Implies(condition, result))
Exists([x], z3.And(condition1, condition2))
# Function declarations
verify = z3.Function("verify", z3.BitVecSort(N), AtomSort, z3.BoolSort())
# Solver usage
solver = z3.Solver()
solver.add(constraints)
if solver.check() == z3.sat:
model = solver.model()
value = model.evaluate(expression)
Error Recovery
Import Errors
# Verify PYTHONPATHecho$PYTHONPATH# Should include Code/src# Test import
PYTHONPATH=Code/src python -c "from model_checker import BuildExample"
