agent_logic.proofs.sequent_calculus

Classes

`Sequent`(**data)	Represents a sequent in sequent calculus: Γ ⊢ Δ (Hypotheses imply conclusions)
`SequentCalculus`()	Implements sequent calculus inference rules for formal proofs.

class agent_logic.proofs.sequent_calculus.Sequent(**data)[source]

Bases: BaseModel

Represents a sequent in sequent calculus: Γ ⊢ Δ (Hypotheses imply conclusions)

Parameters:

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

class agent_logic.proofs.sequent_calculus.SequentCalculus[source]

Bases: object

Implements sequent calculus inference rules for formal proofs.

static and_left(seq)[source]

∧-Left Rule: If (A ∧ B) appears in the hypotheses, split into two sequents: (A ∧ B), Γ ⊢ Δ ⟹ (A, B, Γ ⊢ Δ)

static and_right(seq)[source]

∧-Right Rule: If both A and B appear in the conclusions, merge them into (A ∧ B): Γ ⊢ A, B ⟹ Γ ⊢ (A ∧ B)

static implies_left(seq)[source]

→-Left Rule: If (A → B) is in the hypotheses, transform into two sequents: (A → B), Γ ⊢ Δ ⟹ (Γ ⊢ A) and (B, Γ ⊢ Δ)

static implies_right(seq)[source]

→-Right Rule: If B appears in the conclusions, infer (A → B): Γ, A ⊢ B ⟹ Γ ⊢ (A → B)

static not_left(seq)[source]

¬-Left Rule: If ¬A is in the hypotheses, transform into: (¬A), Γ ⊢ Δ ⟹ Γ ⊢ A, Δ

static not_right(seq)[source]

¬-Right Rule: If A is in the conclusions, infer ¬A: Γ ⊢ A ⟹ Γ, ¬A ⊢ ⊥

static or_left(seq)[source]

∨-Left Rule: If (A ∨ B) is in the hypotheses, generate two cases: (A ∨ B), Γ ⊢ Δ ⟹ (A, Γ ⊢ Δ) and (B, Γ ⊢ Δ)

static or_right(seq)[source]

∨-Right Rule: If A is in the conclusions, we can infer (A ∨ B): Γ ⊢ A ⟹ Γ ⊢ (A ∨ B)