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.AbstractSyntaxTree, Bool}}}:
 [PAndQ.AbstractSyntaxTree(:p) => 1]
 [PAndQ.AbstractSyntaxTree(:p) => 0]

julia> @atomize collect(valuations(p ∧ q))
2×2 Matrix{Vector{Pair{PAndQ.AbstractSyntaxTree, Bool}}}:
 [AbstractSyntaxTree(:p)=>1, AbstractSyntaxTree(:q)=>1]  …  [AbstractSyntaxTree(:p)=>1, AbstractSyntaxTree(:q)=>0]
 [AbstractSyntaxTree(:p)=>0, AbstractSyntaxTree(:q)=>1]     [AbstractSyntaxTree(:p)=>0, AbstractSyntaxTree(: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; solver = Z3)

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.

The solver can be either Z3 or PicoSAT.

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

PAndQ.is_equivalent — Function

is_equivalent(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 is_equivalent(⊥, p ∧ ¬p)
true

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

julia> @atomize is_equivalent($1, $1)
true

julia> @atomize is_equivalent(p, ¬p)
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