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 |
|
clause_and_literal(clause_, literal)
Conjunction of a clause and literal.
Source code in normal_form/prop.py
19 20 21 |
|
clause_or_clause(clause1, clause2)
Disjunction of a Cnf and a Cnf.
Source code in normal_form/prop.py
58 59 60 |
|
clause_or_literal(clause_, literal)
Disjunction of a Cnf and a Cnf.
Source code in normal_form/prop.py
53 54 55 |
|
cnf_and_clause(cnf1, clause_)
Conjunction of a Cnf and a clause.
Source code in normal_form/prop.py
34 35 36 |
|
cnf_and_cnf(cnf1, cnf2)
Conjunction of a Cnf and a Cnf.
Source code in normal_form/prop.py
39 40 41 |
|
cnf_and_literal(cnf1, literal)
Conjuncton of a Cnf and a literal.
Source code in normal_form/prop.py
29 30 31 |
|
cnf_or_clause(cnf1, clause_)
Disjunction of a Cnf and a Cnf.
Source code in normal_form/prop.py
68 69 70 |
|
cnf_or_cnf(cnf1, cnf2)
Disjunction of a Cnf and a Cnf.
Source code in normal_form/prop.py
73 74 75 |
|
cnf_or_literal(cnf1, literal)
Disjunction of a Cnf and a Cnf.
Source code in normal_form/prop.py
63 64 65 |
|
literal_and_literal(literal1, literal2)
Conjunction of a literal and a literal.
Source code in normal_form/prop.py
14 15 16 |
|
literal_or_literal(literal1, literal2)
Disjunction of a Cnf and a Cnf.
Source code in normal_form/prop.py
48 49 50 |
|
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 |
|
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 |
|