agent_logic.proofs.inference_rules
Classes
Extends formal rules of inference for proofs with additional logical principles. |
- class agent_logic.proofs.inference_rules.InferenceRules[source]
Bases:
objectExtends 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:
- Parameters:
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:
- Parameters:
- static associative_rule(expression)[source]
Associative Law: (P ∨ (Q ∨ R)) ≡ ((P ∨ Q) ∨ R) (P ∧ (Q ∧ R)) ≡ ((P ∧ Q) ∧ R)
- Return type:
- 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:
- 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:
- 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:
- 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:
- 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:
- 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:
- 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:
- 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:
- 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:
- Parameters:
- 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:
- Parameters:
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:
- 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:
- 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:
- 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:
- 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:
- Parameters:
p_implies_q (LogicalExpression)
q_implies_r (LogicalExpression)