agent_logic.proofs.quantifier_rules

Classes

QuantifierRules()

Inference rules for quantifiers (∀, ∃).

class agent_logic.proofs.quantifier_rules.QuantifierRules

Bases: object

Inference rules for quantifiers (∀, ∃).

static existential_generalization(predicate, variable)

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

Return type:

ExistentialQuantifier

Parameters:

• predicate (Relation)

• variable (str)

static existential_instantiation(quantifier, constant)

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

Return type:

Relation

Parameters:

• quantifier (ExistentialQuantifier)

• constant (str)

static universal_elimination(quantifier, constant)

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

Return type:

Relation

Parameters:

• quantifier (UniversalQuantifier)

• constant (str)