agent_logic.proofs

Logical proofs module.

This module provides tools for constructing and validating logical proofs, including inference rules and proof verification systems.

class agent_logic.proofs.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:
static addition(p, q)[source]

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

Return type:

LogicalExpression

Parameters:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
class agent_logic.proofs.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 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.proofs.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.proofs.QuantifierRules[source]

Bases: object

Inference rules for quantifiers (∀, ∃).

static existential_generalization(predicate, variable)[source]

P(a) ⊢ ∃x P(x) Replace a constant with a quantified variable.

Return type:

ExistentialQuantifier

Parameters:
static existential_instantiation(quantifier, constant)[source]

∃x P(x) ⊢ P(a) Introduce a fresh constant.

Return type:

Relation

Parameters:
static universal_elimination(quantifier, constant)[source]

∀x P(x) ⊢ P(a) Replace variable x with constant a.

Return type:

Relation

Parameters:
class agent_logic.proofs.Unification[source]

Bases: object

Handles unification for first-order logic terms.

static unify(term1, term2)[source]

Unifies two predicates by finding a substitution θ such that term1(θ) = term2(θ). .. rubric:: Example

P(x) and P(f(y)) → {x → f(y)}

Return type:

Optional[Dict[str, str]]

Parameters:

Modules

combinatorial_proofs

inference_rules

proof_system

Proof system module for logical reasoning.

quantifier_rules

sequent_calculus

unification