Skip to content

prop.py

prop.py

Functions for propositional calculus -- conjunction, disjunction and negation.

clause_and_clause(clause1, clause2)

Conjunction of a clause and a clause.

Source code in normal_form/prop.py
24
25
26
def clause_and_clause(clause1: Clause, clause2: Clause) -> Cnf:
    """Conjunction of a clause and a clause."""
    return cnf([clause1, clause2])

clause_and_literal(clause_, literal)

Conjunction of a clause and literal.

Source code in normal_form/prop.py
19
20
21
def clause_and_literal(clause_: Clause, literal: Lit) -> Cnf:
    """Conjunction of a clause and literal."""
    return cnf([clause_, [literal]])

clause_or_clause(clause1, clause2)

Disjunction of a Cnf and a Cnf.

Source code in normal_form/prop.py
58
59
60
def clause_or_clause(clause1: Clause, clause2: Clause) -> Clause:
    """Disjunction of a Cnf and a Cnf."""
    return clause(clause1 | clause2)

clause_or_literal(clause_, literal)

Disjunction of a Cnf and a Cnf.

Source code in normal_form/prop.py
53
54
55
def clause_or_literal(clause_: Clause, literal: Lit) -> Clause:
    """Disjunction of a Cnf and a Cnf."""
    return clause(clause_ | {literal})

cnf_and_clause(cnf1, clause_)

Conjunction of a Cnf and a clause.

Source code in normal_form/prop.py
34
35
36
def cnf_and_clause(cnf1: Cnf, clause_: Clause) -> Cnf:
    """Conjunction of a Cnf and a clause."""
    return cnf(cnf1 | {clause_})

cnf_and_cnf(cnf1, cnf2)

Conjunction of a Cnf and a Cnf.

Source code in normal_form/prop.py
39
40
41
def cnf_and_cnf(cnf1: Cnf, cnf2: Cnf) -> Cnf:
    """Conjunction of a Cnf and a Cnf."""
    return cnf(cnf1 | cnf2)

cnf_and_literal(cnf1, literal)

Conjuncton of a Cnf and a literal.

Source code in normal_form/prop.py
29
30
31
def cnf_and_literal(cnf1: Cnf, literal: Lit) -> Cnf:
    """Conjuncton of a Cnf and a literal."""
    return cnf(cnf1 | {(literal, )})

cnf_or_clause(cnf1, clause_)

Disjunction of a Cnf and a Cnf.

Source code in normal_form/prop.py
68
69
70
def cnf_or_clause(cnf1: Cnf, clause_: Clause) -> Cnf:
    """Disjunction of a Cnf and a Cnf."""
    return cnf([clause_or_clause(clause1, clause_) for clause1 in cnf1])

cnf_or_cnf(cnf1, cnf2)

Disjunction of a Cnf and a Cnf.

Source code in normal_form/prop.py
73
74
75
def cnf_or_cnf(cnf1: Cnf, cnf2: Cnf) -> Cnf:
    """Disjunction of a Cnf and a Cnf."""
    return ft.reduce(cnf_and_cnf, (cnf_or_clause(cnf1, clause) for clause in cnf2))

cnf_or_literal(cnf1, literal)

Disjunction of a Cnf and a Cnf.

Source code in normal_form/prop.py
63
64
65
def cnf_or_literal(cnf1: Cnf, literal: Lit) -> Cnf:
    """Disjunction of a Cnf and a Cnf."""
    return cnf([clause_or_literal(clause, literal) for clause in cnf1])

literal_and_literal(literal1, literal2)

Conjunction of a literal and a literal.

Source code in normal_form/prop.py
14
15
16
def literal_and_literal(literal1: Lit, literal2: Lit) -> Cnf:
    """Conjunction of a literal and a literal."""
    return cnf([[literal1], [literal2]])

literal_or_literal(literal1, literal2)

Disjunction of a Cnf and a Cnf.

Source code in normal_form/prop.py
48
49
50
def literal_or_literal(literal1: Lit, literal2: Lit) -> Clause:
    """Disjunction of a Cnf and a Cnf."""
    return clause([literal1, literal2])

neg_clause(clause1)

Negate a Clause by distributing negation across literals and returning resulting Cnf.

Example

negation of (a ∨ b ∨ ¬ c) = ¬(a ∨ b ∨ ¬ c) = (¬ a ∧ ¬ b ∧ c) : Cnf.

This function is an almost-involution in the sense that two negations return us back to the original clause, but we pass through an intermediate Cnf-instance.

Source code in normal_form/prop.py
82
83
84
85
86
87
88
89
90
91
def neg_clause(clause1: Clause) -> Cnf:
    """Negate a Clause by distributing negation across literals and returning resulting Cnf.

    Example:
        negation of (a ∨ b ∨ ¬ c) = ¬(a ∨ b ∨ ¬ c) = (¬ a ∧ ¬ b ∧ c) : Cnf.

    This function is an almost-involution in the sense that two negations return us back to
    the original clause, but we pass through an intermediate Cnf-instance.
    """
    return cnf(clause([neg(literal)]) for literal in clause1)

neg_cnf(cnf1)

Negate a Cnf by distributing negation across clauses and returning resulting Cnf.

Example

negation of (c₁ ∧ c₂) = ¬(c₁ ∧ c₂) = ¬c₁ ∨ ¬c₂ : Cnf.

This function is an involution.

Source code in normal_form/prop.py
 94
 95
 96
 97
 98
 99
100
101
102
def neg_cnf(cnf1: Cnf) -> Cnf:
    """Negate a Cnf by distributing negation across clauses and returning resulting Cnf.

    Example:
        negation of (c₁ ∧ c₂) = ¬(c₁ ∧ c₂) = ¬c₁ ∨ ¬c₂ : Cnf.

    This function is an involution.
    """
    return ft.reduce(cnf_or_cnf, map(neg_clause, cnf1))

Last update: September 11, 2022