agent_logic

Agent Logic Package.

This package provides tools for propositional logic, proof validation, and logical reasoning. It includes components for defining logical expressions, evaluating truth values, constructing and validating proofs, and working with logical inference rules.

Modules:: core: Core logical expressions and operations proofs: Tools for constructing and validating logical proofs evaluation: Truth table generation and evaluation utils: Utility functions and logging tools

class agent_logic.BinaryOp(**data)[source]

Bases: LogicalExpression

Represents binary logical operations (AND, OR, IMPLIES, IFF).

Binary operations take two logical expressions as operands and combine them according to the specified operator.

Parameters:

left (LogicalExpression)
right (LogicalExpression)
operator (Literal['AND', 'OR', 'IMPLIES', 'IFF'])

left: The left operand of the binary operation.

right: The right operand of the binary operation.

operator: The type of binary operation, one of: - “AND”: logical conjunction (∧) - “OR”: logical disjunction (∨) - “IMPLIES”: logical implication (→) - “IFF”: logical biconditional (↔)

depth()[source]

Returns the depth of the expression tree.

Return type:: int
Returns:: The maximum depth of either operand plus 1.

evaluate(context)[source]

Evaluates the binary operation given a truth assignment.

Parameters:: context (Dict[str, bool]) – Dictionary mapping variable names to truth values. Example: {“P”: True, “Q”: False}
Return type:: bool
Returns:: Boolean result of applying the binary operation to the operands.
Raises:: ValueError – If the operator is unknown.

classmethod from_dict(data)[source]

Reconstructs a binary operation from a dictionary.

Parameters:: data (Dict) – Dictionary representation of a binary operation. Must contain “left”, “right”, and “operator” fields.
Return type:: BinaryOp
Returns:: Reconstructed BinaryOp object.
Raises:: ValueError – If the data is invalid or contains unknown operand types.

left: LogicalExpression

model_config: ClassVar[ConfigDict] = {'arbitrary_types_allowed': True}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

operator: Literal['AND', 'OR', 'IMPLIES', 'IFF']

right: LogicalExpression

to_dict()[source]

Converts the binary operation to a dictionary.

Return type:: Dict
Returns:: Dictionary representation of the binary operation. Example: {“type”: “BinaryOp”, “left”: {“type”: “Proposition”, “name”: “P”}, “right”: {“type”: “Proposition”, “name”: “Q”}, “operator”: “AND”}

variables()[source]

Returns the list of variables in the binary operation.

Return type:: List[str]
Returns:: List of unique variable names from both operands.

class agent_logic.InferenceRules[source]

Bases: object

Extends formal rules of inference for proofs with additional logical principles.

static absorption(p, p_implies_q)[source]

Absorption Rule: (P → Q) implies (P → (P ∧ Q)). P → Q ⊢ P → (P ∧ Q)

Return type:

LogicalExpression

Parameters:

p (LogicalExpression)
p_implies_q (LogicalExpression)

static addition(p, q)[source]

Addition: If P is true, then (P ∨ Q) must be true. P ⊢ (P ∨ Q)

Return type:

LogicalExpression

Parameters:

p (LogicalExpression)
q (LogicalExpression)

static associative_rule(expression)[source]

Associative Law: (P ∨ (Q ∨ R)) ≡ ((P ∨ Q) ∨ R) (P ∧ (Q ∧ R)) ≡ ((P ∧ Q) ∧ R)

Return type:: LogicalExpression
Parameters:: expression (LogicalExpression)

static biconditional_elimination(p_iff_q)[source]

Biconditional Elimination: If (P ↔ Q) is true, then (P → Q) and (Q → P) must be true. (P ↔ Q) ⊢ (P → Q), (Q → P)

Return type:: List[LogicalExpression]
Parameters:: p_iff_q (LogicalExpression)

static biconditional_introduction(p_implies_q, q_implies_p)[source]

Biconditional Introduction: If (P → Q) is true and (Q → P) is true, then (P ↔ Q) must be true. (P → Q), (Q → P) ⊢ (P ↔ Q)

Return type:

LogicalExpression

Parameters:

p_implies_q (LogicalExpression)
q_implies_p (LogicalExpression)

static conjunction_elimination(p_and_q)[source]

Conjunction Elimination: If (P ∧ Q) is true, then P and Q must be true separately. (P ∧ Q) ⊢ P, Q

Return type:: List[LogicalExpression]
Parameters:: p_and_q (LogicalExpression)

static conjunction_introduction(p, q)[source]

Conjunction Introduction: If P is true and Q is true, then (P ∧ Q) is true. P, Q ⊢ (P ∧ Q)

Return type:

LogicalExpression

Parameters:

p (LogicalExpression)
q (LogicalExpression)

static constructive_dilemma(p_implies_q, r_implies_s, p_or_r)[source]

Constructive Dilemma: If (P → Q) is true, (R → S) is true, and (P ∨ R) is true, then (Q ∨ S) must be true. (P → Q), (R → S), (P ∨ R) ⊢ (Q ∨ S)

Return type:

LogicalExpression

Parameters:

p_implies_q (LogicalExpression)
r_implies_s (LogicalExpression)
p_or_r (LogicalExpression)

static constructive_negation(p_implies_false)[source]

Constructive Negation: If (P → ⊥) is true, then ¬P must be true. (P → ⊥) ⊢ ¬P

Return type:: Not
Parameters:: p_implies_false (LogicalExpression)

static destructive_dilemma(p_implies_q, r_implies_s, not_q_or_not_s)[source]

Destructive Dilemma: If (P → Q) is true, (R → S) is true, and (¬Q ∨ ¬S) is true, then (¬P ∨ ¬R) must be true. (P → Q), (R → S), (¬Q ∨ ¬S) ⊢ (¬P ∨ ¬R)

Return type:

LogicalExpression

Parameters:

p_implies_q (LogicalExpression)
r_implies_s (LogicalExpression)
not_q_or_not_s (LogicalExpression)

static disjunctive_syllogism(p_or_q, not_p)[source]

Disjunctive Syllogism: If (P ∨ Q) is true and ¬P is true, then Q must be true. (P ∨ Q), ¬P ⊢ Q

Return type:

LogicalExpression

Parameters:

p_or_q (LogicalExpression)
not_p (LogicalExpression)

static distributive_rule(expression)[source]

Distributive Law: (P ∧ (Q ∨ R)) ≡ ((P ∧ Q) ∨ (P ∧ R)) (P ∨ (Q ∧ R)) ≡ ((P ∨ Q) ∧ (P ∨ R))

Return type:: LogicalExpression
Parameters:: expression (LogicalExpression)

static hypothetical_syllogism(p_implies_q, q_implies_r)[source]

Hypothetical Syllogism: If (P → Q) is true and (Q → R) is true, then (P → R) must be true. (P → Q), (Q → R) ⊢ (P → R)

Return type:

LogicalExpression

Parameters:

p_implies_q (LogicalExpression)
q_implies_r (LogicalExpression)

static law_of_excluded_middle(p)[source]

Law of Excluded Middle: P ∨ ¬P is always true. ⊢ (P ∨ ¬P)

Return type:: BinaryOp
Parameters:: p (LogicalExpression)

static modus_ponens(p, p_implies_q)[source]

Modus Ponens: If P is true and (P → Q) is true, then Q must be true. P, (P → Q) ⊢ Q

Return type:

LogicalExpression

Parameters:

p (LogicalExpression)
p_implies_q (LogicalExpression)

static modus_tollens(not_q, p_implies_q)[source]

Modus Tollens: If ¬Q is true and (P → Q) is true, then ¬P must be true. ¬Q, (P → Q) ⊢ ¬P

Return type:

LogicalExpression

Parameters:

not_q (LogicalExpression)
p_implies_q (LogicalExpression)

static negation_elimination(not_not_p)[source]

Negation Elimination: If ¬(¬P) is true, then P must be true. ¬(¬P) ⊢ P

Return type:: LogicalExpression
Parameters:: not_not_p (LogicalExpression)

static negation_introduction(p_implies_false)[source]

Negation Introduction: If (P → ⊥) is true, then ¬P must be true. (P → ⊥) ⊢ ¬P

Return type:: LogicalExpression
Parameters:: p_implies_false (LogicalExpression)

static proof_by_contradiction(assumption, contradiction)[source]

Reductio ad Absurdum (Proof by Contradiction): If assuming P leads to ⊥, then ¬P must be true. P ⊢ ⊥ ⟹ ¬P

Return type:

Not

Parameters:

assumption (LogicalExpression)
contradiction (LogicalExpression)

static transitivity_of_implication(p_implies_q, q_implies_r)[source]

Transitivity of Implication: If (P → Q) and (Q → R) hold, then (P → R) holds. (P → Q), (Q → R) ⊢ (P → R)

Return type:

LogicalExpression

Parameters:

p_implies_q (LogicalExpression)
q_implies_r (LogicalExpression)

class agent_logic.LogicalExpression(**data)[source]

Bases: BaseModel

Recursive base class for logical expressions.

This abstract class defines the interface for all logical expressions in the system. Concrete implementations include Proposition, Not, and BinaryOp.

model_config: Pydantic model configuration to allow arbitrary types.

depth()[source]

Computes the depth of the logical expression tree.

Return type:: int
Returns:: Integer representing the depth of the expression tree.
Raises:: NotImplementedError – This is an abstract method that must be implemented by subclasses.

evaluate(context)[source]

Recursively evaluates the expression under a given truth assignment.

Parameters:: context (Dict[str, bool]) – Dictionary mapping variable names to truth values. Example: {“P”: True, “Q”: False}
Return type:: bool
Returns:: Boolean result of evaluating the expression.
Raises:: NotImplementedError – This is an abstract method that must be implemented by subclasses.

classmethod from_dict(data)[source]

Recursively reconstructs an expression from a dictionary.

Parameters:: data (Dict) – Dictionary representation of a logical expression. Must include a ‘type’ field.
Return type:: LogicalExpression
Returns:: Reconstructed logical expression.
Raises:: ValueError – If the data is not a dictionary, doesn’t have a type field, or has an unknown expression type.

model_config: ClassVar[ConfigDict] = {'arbitrary_types_allowed': True}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

to_dict()[source]

Recursively converts expression to a dictionary.

Return type:: Dict
Returns:: Dictionary representation of the logical expression.
Raises:: NotImplementedError – This is an abstract method that must be implemented by subclasses.

variables()[source]

Recursively extracts all variables in the expression.

Return type:: List[str]
Returns:: List of variable names used in the expression.
Raises:: NotImplementedError – This is an abstract method that must be implemented by subclasses.

class agent_logic.Not(**data)[source]

Bases: LogicalExpression

Represents logical negation (¬).

The NOT operation negates the truth value of its operand.

Parameters:: operand (LogicalExpression)

operand: The logical expression being negated.

depth()[source]

Returns the depth of the expression tree.

Return type:: int
Returns:: The depth of the operand plus 1.

evaluate(context)[source]

Evaluates the NOT expression given a truth assignment.

Parameters:: context (Dict[str, bool]) – Dictionary mapping variable names to truth values. Example: {“P”: True, “Q”: False}
Return type:: bool
Returns:: Boolean result of negating the operand’s evaluation.

classmethod from_dict(data)[source]

Reconstructs a NOT expression from a dictionary.

Parameters:: data (Dict) – Dictionary representation of a NOT expression. Must contain an “operand” field.
Return type:: Not
Returns:: Reconstructed Not object.
Raises:: ValueError – If the data is invalid or contains an unknown operand type.

model_config: ClassVar[ConfigDict] = {'arbitrary_types_allowed': True}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

operand: LogicalExpression

to_dict()[source]

Converts the NOT expression to a dictionary.

Return type:: Dict
Returns:: Dictionary representation of the NOT expression. Example: {“type”: “Not”, “operand”: {“type”: “Proposition”, “name”: “P”}}

variables()[source]

Returns the list of variables in the NOT expression.

Return type:: List[str]
Returns:: List of variable names used in the operand.

class agent_logic.Proof(**data)[source]

Bases: BaseModel

Represents a structured proof with step-by-step reasoning.

A proof consists of a sequence of steps, each building on previous steps according to valid rules of inference. The proof is valid if each step follows logically from the steps it depends on.

Parameters:

steps (List[ProofStep])
debug (bool)

steps: List of ProofStep objects making up the proof.

debug: Boolean flag to enable or disable debug output during validation.

apply_inference(step, known_statements)[source]

Applies inference rules dynamically based on the step’s justification.

Extracts the referenced statements from previous steps, and applies the appropriate inference rule to derive the current step.

Parameters:

step (ProofStep) – The current proof step being validated.
known_statements (Dict[int, LogicalExpression]) – Dictionary mapping step numbers to their logical expressions.

Return type:

Optional[LogicalExpression]

Returns:

The derived logical expression, or None if inference failed.

debug: bool

classmethod from_dict(data)[source]

Reconstructs a proof from a dictionary representation.

Parameters:: data (Dict) – Dictionary containing a “steps” list with proof step data.
Return type:: Proof
Returns:: Reconstructed Proof object.

is_valid()[source]

Validates the proof by ensuring logical correctness of each step.

The validation process checks that: 1. All referenced dependencies exist 2. Each step follows logically from its dependencies using the specified rule 3. The derived statement matches the claimed statement

Return type:: bool
Returns:: Boolean indicating whether the proof is valid.

model_config: ClassVar[ConfigDict] = {}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

steps: List[ProofStep]

to_dict()[source]

Serializes the proof to a structured dictionary for external usage.

Return type:: Dict
Returns:: Dictionary representation of the proof with all steps.

class agent_logic.ProofStep(**data)[source]

Bases: BaseModel

Represents a single step in a structured proof.

Each step consists of a logical statement, a justification for that statement, and optional references to previous steps that support the justification.

Parameters:

step_number (int)
statement (LogicalExpression)
justification (str)
dependencies (List[int] | None)

step_number: Sequential number identifying this step in the proof.

statement: The logical expression being asserted at this step.

justification: Name of the inference rule or justification for this step.

dependencies: List of step numbers that this step depends on, or None if this is a premise.

dependencies: Optional[List[int]]

justification: str

model_config: ClassVar[ConfigDict] = {}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

statement: LogicalExpression

step_number: int

class agent_logic.Proposition(**data)[source]

Bases: LogicalExpression

Represents an atomic proposition (logical variable).

An atomic proposition is the most basic unit in propositional logic, representing a statement that can be either true or false.

Parameters:: name (str)

name: The name of the proposition (e.g., “P”, “Q”).

depth()[source]

Returns the depth of the expression tree.

For an atomic proposition, the depth is always 0.

Return type:: int
Returns:: 0, as atomic propositions have no depth.

evaluate(context)[source]

Evaluates the proposition given a truth assignment.

Parameters:: context (Dict[str, bool]) – Dictionary mapping variable names to truth values. Example: {“P”: True, “Q”: False}
Return type:: bool
Returns:: Boolean value of the proposition in the given context.
Raises:: ValueError – If the proposition name is not in the context.

classmethod from_dict(data)[source]

Reconstructs a proposition from a dictionary.

Parameters:: data (Dict) – Dictionary representation of a proposition. Must contain a “name” field.
Return type:: Proposition
Returns:: Reconstructed Proposition object.

model_config: ClassVar[ConfigDict] = {'arbitrary_types_allowed': True}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

name: str

to_dict()[source]

Converts the proposition to a dictionary.

Return type:: Dict
Returns:: Dictionary representation of the proposition. Example: {“type”: “Proposition”, “name”: “P”}

variables()[source]

Returns the list of variables in the proposition.

Return type:: List[str]
Returns:: A list containing only the name of this proposition.

class agent_logic.TruthTable(expression)[source]

Bases: object

Generates a truth table for a given logical expression.

Parameters:: expression (LogicalExpression)

generate()[source]

Generates all possible truth values for the logical expression.

Return type:: List[Dict[str, Union[bool, str]]]
Returns:: List of dictionaries, where each dictionary represents a row in the truth table.

is_contradiction()[source]

Checks if the expression is always false.

Return type:: bool
Returns:: True if the expression evaluates to False for all assignments, otherwise False.

is_satisfiable()[source]

Checks if there exists a truth assignment that makes the expression true.

Return type:: bool
Returns:: True if at least one assignment makes the expression True, otherwise False.

is_tautology()[source]

Checks if the expression is always true.

Return type:: bool
Returns:: True if the expression evaluates to True for all assignments, otherwise False.

agent_logic.get_logger(name, level=None)[source]

Get a configured logger instance.

Creates or retrieves a logger with the given name and configures it with appropriate formatting and log level.

Parameters:

name (str) – Name of the logger (typically module name)
level (Optional[int]) – Logging level (if None, uses INFO)

Return type:

Logger

Returns:

Configured logger instance ready for use

agent_logic.set_global_log_level(level)[source]

Set the log level for all loggers in the logic package.

This function affects all existing loggers in the logic namespace and sets their level to the specified value.

Parameters:: level (int) – Logging level (DEBUG, INFO, WARNING, ERROR, CRITICAL) Example: logging.DEBUG or logging.ERROR
Return type:: None

Example

>>> from logic.utils.logger import set_global_log_level
>>> import logging
>>> set_global_log_level(logging.DEBUG)  # Enable debug logging

Modules

`cli`	Command-line interface for the agent-logic package.
`core`	Core logical expressions and operations.
`evaluation`	Logical evaluation module.
`models`	Logic models module.
`parsing`	Logic parsing module.
`proofs`	Logical proofs module.
`utils`	Utilities module for the logic package.