Three-Valued Logic

aria.bool.threeval implements propositional reasoning in Kleene’s three-valued logic, where propositions can be true, false, or unknown.

Directory structure

aria/bool/threeval/
├── propositional.py    # Three-valued formula AST and evaluation
├── parser.py           # Parser for three-valued logic expressions
├── adapters.py         # Adapters bridging three-valued and two-valued worlds
└── minimization.py     # Formula minimisation techniques

Three-valued semantics

Formulas are evaluated under Kleene strong three-valued logic:

true ∧ unknown = unknown
false ∧ unknown = false
true ∨ unknown = true
false ∨ unknown = unknown

This is useful for reasoning about partial models, over-approximations, and verification scenarios where some propositions are undetermined.

Key components

Propositional (propositional.py) – defines the three-valued formula AST and truth-table evaluation engine.
Parser (parser.py) – textual parser for three-valued logic expressions.
Adapters (adapters.py) – bridge utilities that translate between three-valued assignments and classical two-valued SAT/QBF encodings.
Minimisation (minimization.py) – algorithms for simplifying or minimising three-valued formulas.

Programmatic usage

from aria.bool.threeval.propositional import evaluate

# Evaluate a three-valued formula over a partial assignment
result = evaluate(formula, assignment)