pytableaux.proof

Classes

class Branch(parent=None, /)

A tableau branch.

Parameters:

parent (Branch | None) --

property id: int

The branch object id.

property origin: Branch

The root branch.

property closed: bool

Whether the branch is closed.

property leaf: Node | None

The leaf node, if any.

property model: BaseModel | None

The associated model, if any.

property parent: Branch | None

The parent branch, if any.

worlds: Set[int]

The set of worlds on the branch.

constants: Set[Constant]

The set of constants on the branch.

copy(*, parent=None, listeners=False)

Copy of the branch.

Parameters:

• parent (Optional[Branch]) -- The branch to set as the new branch's parent. Defaults to None.

• listeners (bool) -- Whether to copy event listeners. Defaults to False.

Returns:

The new branch.

Return type:

Branch

has(mapping, /)

Whether there is a node on the branch that matches the given properties.

Parameters:

• props (Mapping) -- A mapping of properties.

• mapping (Mapping) --

Returns:

Whether there is a match.

Return type:

bool

any(mappings, /)

Check a list of property mappings against the has method.

Parameters:

mappings (Iterable[Mapping]) -- An iterable of property mappings.

Returns:

True when the first match is found, else False.

Return type:

bool

all(mappings, /)

Check a list of property mappings against the has method.

Parameters:

mappings (Iterable[Mapping]) -- An iterable of property mappings.

Returns:

False when the first non-match is found, else True.

Return type:

bool

find(mapping, /)

Find the first node on the branch that matches the given properties.

Parameters:

• props (Mapping) -- A mapping of properties.

• mapping (Mapping) --

Returns:

The node, or None if not found.

Return type:

Optional[Node]

search(mapping, /)

Search the nodes on the branch that match the given properties, up to the limit, if given.

Parameters:

• props (Mapping) -- A mapping of properties.

• limit (int) -- An optional result limit.

• mapping (Mapping) --

Returns:

Results generator.

Return type:

Generator[Node]

append(node, /)

Append a node.

Parameters:

node (Mapping) -- Node object or mapping.

Returns:

self

Return type:

Branch

Raises:

DuplicateValueError -- if the node is already on the branch.

extend(nodes, /)

Add multiple nodes.

Parameters:

nodes (Iterable) -- An iterable of node objects/mappings.

Returns:

self

Return type:

Branch

Raises:

DuplicateValueError -- if a node is already on the branch.

tick(node, /)

Tick a node for the branch.

Parameters:

node (Node) -- The node to tick.

Returns:

self

Return type:

Branch

close()

Close the branch. Adds a flag node and emits the AFTER_BRANCH_CLOSE event.

Returns:

self.

Return type:

Branch

is_ticked(node, /)

Whether the node is ticked relative to the branch.

Parameters:

node (Node) -- The node instance.

Return type:

bool

Returns

bool: Whether the node is ticked.

new_constant()

Return a new constant that does not appear on the branch.

Returns:

The new constant.

Return type:

Constant

new_world()

Return a new world that does not appear on the branch.

Returns:

A new word.

Return type:

int

class Index(indexes)

Branch node index.

Parameters:

indexes (Iterable[tuple[str, ...]]) --

class Node(mapping=mappingproxy({}), /)

A tableau node.

property id: int

The unique object ID.

worlds()

Yield from int values for world, world1, and world2 keys.

Return type:

Iterator[int]

has(*names)

Whether the node has a non-None property of all the given names.

Return type:

bool

any(*names)

Whether the node has a non-None property of any of the given names.

Return type:

bool

meets(mapping, /)

Whether the node properties match all those given in mapping.

Parameters:

mapping (Mapping) --

Return type:

bool

class Target(*args, **kw)

Rule application target.

class Rule(tableau, /, **opts)

Base class for a Tableau rule.

Parameters:

tableau (Tableau) --

legend: tuple[tuple[str, Any], ...]

The rule class legend.

Helpers: Mapping[type[Rule.Helper], Any] = mappingproxy({})

Helper classes mapped to their settings.

timer_names: Sequence[str] = qsetf({'search', 'apply'})

StopWatch names to create in timers mapping.

name: str = 'Rule'

The rule class name.

ticking: bool = False

Whether this is a ticking rule.

autoattrs: bool | None = None

Whether to induce class attributes from the rule name.

branching: int = 0

The number of additional branches created.

modal: bool | None = None

Whether this is a modal rule.

state: Rule.State

The state bit flag.

tableau: Tableau

The tableau instance.

opts: Mapping

The options.

timers: Mapping[str, StopWatch]

StopWatch instances mapped by name.

history: Sequence[Target]

The targets applied to.

helpers: TypeInstMap[Rule.Helper]

Helper instances mapped by class.

abstract example_nodes()

Return example nodes that would trigger the rule.

Return type:

Iterable[Node]

sentence(node, /)

Get the relevant sentence for the node, or None.

Parameters:

node (Node) --

Return type:

Sentence | None

final target(branch, /)

Get the rule target if it applies.

Parameters:

branch (Branch) --

Return type:

Target | None

final apply(target, /)

Apply the rule to a target returned from .target().

Parameters:

target (Target) --

Return type:

None

classmethod test(*, noassert=False)

Run a simple test on the rule.

class Tableau(logic=None, argument=None, **opts)

A tableau proof.

argument

The argument of the tableau.

When setting this value, if the tableau has a logic set, and the auto_build_trunk option is true (default), then the trunk is automatically built.

logic

The logic of the tableau.

When setting this value, if the tableau has an argument set, and the auto_build_trunk option is true (default), then the trunk is automatically built.

finished

Whether the tableau is finished. A tableau is finished iff any of the following conditions apply:

• The tableau is completed.

• The max_steps option is met or exceeded.

• The build_timeout option is exceeded.

• The finish method is manually invoked.

valid

Whether the tableau's argument is valid (proved). A tableau with an argument is valid iff it is completed and it has no open branches. If the tableau is not completed, or it has no argument, the value will be None.

invalid

Whether the tableau's argument is invalid (disproved). A tableau with an argument is invalid iff it is completed and it has at least one open branch. If the tableau is not completed, or it has no argument, the value will be None.

completed

Whether the tableau is completed. A tableau is completed iff all rules that can be applied have been applied.

premature

Whether the tableau is finished prematurely. A tableau is premature iff it is finished but not completed.

id

The unique object ID of the tableau.

history: Sequence[Tableau.StepEntry]

The history of rule applications.

rules: RulesRoot

The rule instances.

open: SequenceSet[Branch]

Ordered view of the open branches.

tree: Tableau.Tree

A tree structure of the tableau. This is generated after the tableau is finished. If the build_timeout was exceeded, the tree is not built.

build()

Build the tableau. Returns self.

step()

Find, execute, and return the next rule application. If no rule can be applied, the finish() method is called, and None is returned. If the tableau is already finished then this is a no-op and``None`` is returned.

Returns (Tableau.StepEntry):

The history entry, or None.

Return type:

StepEntry | None

stepiter()

Returns an iterator that calls step() until None is returned.

Return type:

Iterator[StepEntry]

branch(parent=None)

Create a new branch on the tableau, as a copy of parent, if given.

Parameters:

parent (Branch) -- The parent branch, if any.

Returns:

The new branch.

Return type:

Branch

add(branch)

Add a new branch to the tableau. Returns self.

Parameters:

branch (Branch) -- The branch to add.

Returns:

self

Return type:

Self

finish()

Mark the tableau as finished, and perform post-build tasks, including populating the tree, stats, and models properties.

When using the build() or step() methods, there is never a need to call this method, since it is handled internally. However, this method is safe to call multiple times. If the tableau is already finished, it will be a no-op.

Returns:

self

Return type:

Self

build_trunk()

Build the trunk of the tableau. Delegates to the build_trunk() method of System. This is called automatically when the tableau has non-empty argument and logic properties and the auto_build_trunk option is True (default).

Raises:

errors.IllegalStateError -- if the trunk is already built, the tableau is already started, there is no argument, or no logic.

Return type:

Self

branching_complexity(node, /)

Caching method for the logic's System.branching_complexity() method. If the tableau has no logic, then 0 is returned.

Parameters:

node (Node) -- The node to evaluate.

Returns:

The branching complexity.

Return type:

int

class System

Tableaux system base class.

abstract classmethod build_trunk(b, arg, /)

Build the trunk for an argument on the tableau.

Parameters:

• b (Branch) -- The branch to construct.

• arg (Argument) -- The argument.

Return type:

None

classmethod branching_complexity(node, rules, /)

Compute how many new branches would be added if a rule were to be applied to the node.

Parameters:

• node (Node) -- The node instance.

• rules (RulesRoot) -- The rules on the tableau.

Returns:

The number of new branches.

Return type:

int

classmethod branching_complexity_hashable(node, /)

Return a hashable object corresponding to a node's branching complexity, in order to save redundant computation time. By default it just returns the node itself.

Parameters:

node (Node) -- The node instance.

Returns:

A hashable object.

Return type:

Hashable

class Tableau.Tree

Recursive tree structure representation of a tableau.

leaf: bool = False

Whether this is a terminal (childless) structure.

closed: bool = False

Whether this is a terminal structure that is closed.

open: bool = False

Whether this is a terminal structure that is open.

left: int = None

The pre-ordered tree left value.

right: int = None

The pre-ordered tree right value.

descendant_node_count: int = 0

The total node count of all descendants.

structure_node_count: int = 0

The node count plus descendant node count.

depth: int = 0

The depth of this structure (ancestor structure count).

has_open: bool = False

Whether this structure or a descendant is open.

has_closed: bool = False

Whether this structure or a descendant is closed.

closed_step: int | None = None

If closed, the step number at which it closed.

step: int = None

The step number at which this structure first appears.

width: int = 0

The number of descendant terminal structures, or 1.

balanced_line_width: float = 0.0

0.5x the width of the first child structure, plus 0.5x the width of the last child structure (if distinct from the first), plus the sum of the widths of the other (distinct) children.

balanced_line_margin: float = 0.0

0.5x the width of the first child structure divided by the width of this structure.

branch_id: int | None = None

The branch id, only set for leaves

model_id: int | None = None

The model id, if exists, only set for leaves

is_only_branch: bool = False

Whether this is the one and only branch

branch_step: int = None

The step at which the branch was added

nodes: list[Node]

The nodes on this structure.

ticksteps: list[int | None]

The ticked steps list.

children: list[Tree]

The child structures.

class Rule.Helper(rule, /)

Rule helper basic base class.

Parameters:

rule (Rule) --

class RulesRoot(tableau, /)

Grouped and named collection of rules for a tableau.

Parameters:

tableau (Tableau) --

groups: RuleGroups

The rule groups sequence view.

append(rulecls, /, name=None)

Add a single Rule to a new group.

Parameters:

• rulecls (type[Rule]) --

• name (str | None) --

extend(classes, /, name=None)

Create a new group from a collection of Rule classes.

Parameters:

• classes (Iterable[type[Rule]]) --

• name (str | None) --

clear()

Clear all the rules. Raises IllegalStateError if tableau is started.

get(ref, default=<object object>, /)

Get rule instance by name or type.

Parameters:

• ref (type[_RT] | str) -- A Rule class or name.

• default -- A value to return if rule not found.

Returns:

The rule instance, or default if it is specified and the rule was not found.

Raises:

• KeyError -- If rule not found and default not passed.

• TypeError -- For bad ref type.

Return type:

_RT

names()

Return all the rule names.

class RuleGroups(root, /)

Parameters:

root (RulesRoot) --

create(name=None)

Create and return a new emtpy rule group.

Parameters:

name (str | None) --

append(classes, /, name=<object object>)

Create a new group with the given rules. Raise IllegalStateError if locked.

Parameters:

• classes (Iterable[type[Rule]]) --

• name (str | None) --

extend(groups)

Add multiple groups. Raise IllegalStateError if locked.

Parameters:

groups (Iterable[Iterable[type[Rule]]]) --

clear()

Clear the groups. Raise IllegalStateError if locked.

Parameters:

self (RulesRoot) --

get(name, default=<object object>, /)

Get a group by name.

Parameters:

name (str) --

Return type:

RuleGroup

names()

List the named groups.

Return type:

Set[str]

class RuleGroup(name, root, /)

A rule group of a Tableau's rules.

This class supports the full Sequence standard interface for iterating, subscripting, and slicing.

The append, extend, and clear methods provide mutability until the instance is locked. An input value is a subclass of Rule, which is instantiated for the tableau before it is added to the sequence.

Rule instances are indexed, and can be retrieved by its class or name using the get method.

Parameters:

• name (str | None) --

• root (RulesRoot) --

name: str | None

The group name.

append(rulecls, /)

Instantiate and append a rule class.

Parameters:

rulecls (type[Rule]) -- A Rule class.

Raises:

• ValueError -- If there is a duplicate name.

• TypeError -- If value is not a subclass of Rule.

• errors.IllegalStateError -- If locked.

extend(classes, /)

Append multiple rules.

Parameters:

classes (Iterable[type[Rule]]) -- An iterable of Rule classes.

Raises:

• ValueError -- If there is a duplicate name.

• TypeError -- If an element is not a subclass of Rule.

• errors.IllegalStateError -- If locked.

clear()

Clear the rule group.

Raises:

errors.IllegalStateError -- If locked.

Parameters:

self (RulesRoot) --

get(ref: str, default=<object object>) → Rule

get(ref: type[_RT]) → _RT

Get rule instance by name or type.

Parameters:

• ref -- A Rule class or name.

• default -- A value to return if rule not found.

Returns:

The rule instance, or default if it is specified and the rule was not found.

Raises:

• KeyError -- If rule not found and default not passed.

• TypeError -- For bad ref type.

names()

Return all the rule names.