ARBITER v0.1

A propositional logic validation and compression library.

Installation

pip install .

For development:

pip install -e ".[dev]"

Usage

from arbiter import validate, compress, entails

# Validate a rule set
result = validate(["a -> b", "b -> c"])
print(result.valid)  # True
print(result.parse_errors)  # []
print(result.contradictions)  # []

# Check for contradictions
result = validate(["a", "!a"])
print(result.valid)  # False
print(result.contradictions)  # [Contradiction(...)]

# Compress redundant rules
result = compress(["a -> b", "b -> c", "a -> c"])
print(result.original_count)  # 3
print(result.compressed_count)  # 2
print(result.minimal_rules)  # ["a -> b", "b -> c"]

# Check entailment
assert entails(["a -> b", "a"], "b") is True
assert entails(["a -> b"], "b") is False

Grammar

Rules follow the arbiter_v0 grammar:

rule: expr "->" expr

expr: or_expr
or_expr: and_expr ("|" and_expr)*
and_expr: unary_expr ("&" unary_expr)*
unary_expr: "!" unary_expr | atom
atom: "(" expr ")" | comparison | IDENTIFIER

comparison: IDENTIFIER ("==" | "!=" | "<" | ">" | "<=" | ">=") value
value: STRING | NUMBER | BOOLEAN

IDENTIFIER: /[a-zA-Z][a-zA-Z0-9_]*/
STRING: "'" /[^']*/ "'"
NUMBER: /-?[0-9]+(\.[0-9]+)?/
BOOLEAN: "true" | "false"

Examples

• Simple implication: a -> b
• Conjunction: a & b -> c
• Disjunction: a | b -> c
• Negation: !a -> b
• Comparison: role == 'admin' -> can_delete
• Numeric: retries > 3 -> locked
• Complex: (a | b) & !c -> d | e

Development

Run tests:

pytest

Run with coverage:

pytest --cov=arbiter --cov-report=term-missing

Type checking:

mypy --strict arbiter

License

MIT