Semantics

Truths

PAndQ.valuations — Function

valuations(atoms)
valuations(p)

Return an iterator of every possible valuation of the given atoms or the atoms contained in p.

Examples

julia> collect(valuations(⊤))
0-dimensional Array{Vector{Union{}}, 0}:
[]

julia> @atomize collect(valuations(p))
2-element Vector{Vector{Pair{PAndQ.Variable, Bool}}}:
 [PAndQ.Variable(:p) => 1]
 [PAndQ.Variable(:p) => 0]

julia> @atomize collect(valuations(p ∧ q))
2×2 Matrix{Vector{Pair{PAndQ.Variable, Bool}}}:
 [Variable(:p)=>1, Variable(:q)=>1]  [Variable(:p)=>1, Variable(:q)=>0]
 [Variable(:p)=>0, Variable(:q)=>1]  [Variable(:p)=>0, Variable(:q)=>0]

source

PAndQ.interpret — Function

interpret(valuation, p)

Substitute each atom in p with values given by the valuation.

The valuation can be a Function that accepts an atom and returns a logical value, a Dictionary mapping from atoms to logical values, or an iterable that can construct such a dictionary. No substitution is performed if an atom is not one of the dictionary's keys.

Examples

julia> @atomize interpret(atom -> ⊤, ¬p)
¬⊤

julia> @atomize interpret(p => ⊤, p ∧ q)
⊤ ∧ q

source

PAndQ.interpretations — Function

interpretations(valuations, p)
interpretations(p)

Return an Array{Bool} given by interpreting p with each of the valuations.

Examples

julia> collect(interpretations(⊤))
0-dimensional Array{Bool, 0}:
1

julia> @atomize collect(interpretations(p))
2-element Vector{Bool}:
 1
 0

julia> @atomize collect(interpretations(p ∧ q))
2×2 Matrix{Bool}:
 1  0
 0  0

source

PAndQ.solutions — Function

solutions(p)

Return a stateful iterator of valuations such that interpret(valuation, p) == ⊤.

To find every valuation that results in a true interpretation, convert the proposition to conjunctive normal form using normalize. Otherwise, a subset of those valuations will be identified using the tseytin transformation.

Predicates

PAndQ.is_tautology — Function

is_tautology(p)

Return a Boolean indicating whether the given proposition is logically equivalent to a tautology.

Examples

julia> is_tautology(⊤)
true

julia> @atomize is_tautology(p)
false

julia> @atomize is_tautology(¬(p ∧ ¬p))
true

source

PAndQ.is_contradiction — Function

is_contradiction(p)

Return a Boolean indicating whether the given proposition is logically equivalent to a contradiction.

Examples

julia> is_contradiction(⊥)
true

julia> @atomize is_contradiction(p)
false

julia> @atomize is_contradiction(p ∧ ¬p)
true

source

PAndQ.is_truth — Function

is_truth(p)

Return a Boolean indicating whether given proposition is logically equivalent to a truth value.

Examples

julia> is_truth(⊤)
true

julia> @atomize is_truth(p ∧ ¬p)
true

julia> @atomize is_truth(p)
false

julia> @atomize is_truth(p ∧ q)
false

source

PAndQ.is_contingency — Function

is_contingency(p)

Return a Boolean indicating whether p is a contingency (not logically equivalent to a truth value).

Examples

julia> is_contingency(⊤)
false

julia> @atomize is_contingency(p ∧ ¬p)
false

julia> @atomize is_contingency(p)
true

julia> @atomize is_contingency(p ∧ q)
true

source

PAndQ.is_satisfiable — Function

is_satisfiable(p)

Return a Boolean indicating whether p is satisfiable (not logically equivalent to a contradiction).

Examples

julia> is_satisfiable(⊤)
true

julia> @atomize is_satisfiable(p ∧ ¬p)
false

julia> @atomize is_satisfiable(p)
true

julia> @atomize is_satisfiable(p ∧ q)
true

source

PAndQ.is_falsifiable — Function

is_falsifiable(p)

Return a Boolean indicating whether p is falsifiable (not logically equivalent to a tautology).

Examples

julia> is_falsifiable(⊥)
true

julia> @atomize is_falsifiable(p ∨ ¬p)
false

julia> @atomize is_falsifiable(p)
true

julia> @atomize is_falsifiable(p ∧ q)
true

source

PAndQ.is_equisatisfiable — Function

is_equisatisfiable(p, q)

Return a Boolean indicating whether the predicate is_satisfiable is congruent for both propositions.

Examples

julia> is_equisatisfiable(⊤, ⊥)
false

julia> @atomize is_equisatisfiable(p, q)
true

source

Ordering

Propositions and their truth values have a strict partial order. The truth values tautology and contradiction are the top and bottom of this order, respectively. A proposition that satisfies the predicate is_tautology or is_contradiction is also at the top or bottom of the order, respectively. Propositions that satisfy the predicate is_contingency occupy the middle of this order. In other words, ⊥ < ⊤, ⊥ <= p, and p <= ⊤ for some proposition p. The ordering is partial because the predicates == and is_truth may both be false for two given propositions.

Note

The implementations for == and < also define the semantics of isequal, >, <=, and >=. This does not define the semantics of isless, which is used for total orders.

Warning

The assumption that isequal(p, q) implies hash(p) == hash(q) is currently being violated. A future version will implement the Quine–McCluskey algorithm to minimize propositions, which will enable hash to be defined too.

Base.:== — Function

==(p, q)
p == q

Return a Boolean indicating whether p and q are logically equivalent.

Constants are equivalent only if their values are equivalent.

Info

The ≡ symbol is sometimes used to represent logical equivalence. However, Julia uses ≡ as an alias for the builtin function === which cannot have methods added to it.

Examples

julia> @atomize ⊥ == p ∧ ¬p
true

julia> @atomize (p ↔ q) == ¬(p ↮ q)
true

julia> @atomize $1 == $1
true

julia> @atomize p == ¬p
false

source

Base.:< — Function

<(p, q)
p < q

Return a Boolean indicating whether the arguments are ordered such that r < s < t, where r, s, and t satisfy is_contradiction, is_contingency, and is_tautology, respectively.

Examples

julia> @atomize ⊥ < p < ⊤
true

julia> @atomize p ∧ ¬p < p < p ∨ ¬p
true

julia> @atomize p < p
false

julia> ⊤ < ⊥
false

source

Utilities

Core.Bool — Method

Bool(truth_value)

Return a Boolean corresponding to the given truth value.

Examples

julia> Bool(⊤)
true

julia> Bool(⊥)
false

source