Propositions

Instantiation

PAndQ.@atomize — Macro

@atomize(x)

Instantiate constants and variables inline.

Constants are instantiated with the $ interpolation syntax. Variables are instantiated with previously undefined symbols.

Warning

This macro attempts to ignore symbols that are being assigned a value. For example, @atomize f(; x = p) = x ∧ q should be equivalent to f(; x = @atomize p) = x ∧ @atomize q. However, this feature is in-progress and only works in some cases. The implementation is cautious to skip the parts of the expression that it cannot yet handle.

Examples

julia> @atomize x = p ∧ q
p ∧ q

julia> @atomize x → r
(p ∧ q) → r

julia> @atomize $1 ∧ $(1 + 1)
$(1) ∧ $(2)

source

PAndQ.@variables — Macro

@variables(ps...)

Define variables and return a Vector containing them.

Examples

julia> @variables p q
2-element Vector{PAndQ.Variable}:
 p
 q

julia> p
p

julia> q
q

source

PAndQ.constants — Function

constants(f = 𝒾, xs)

Equivalent to map(x -> @atomize $(f(x)), xs).

Utilities

PAndQ.value — Function

value(T = Any, p)

If p is logically equivalent to a constant, return that constant's value wrapped in Some. Otherwise, return nothing.

Values wrapped in Some can be unwrapped using the something function.

Tip

To reduce compilation latency, constants do not store the type of the wrapped value. Therefore, the type of this value cannot be inferred and can result in run-time dispatch. If this type is known at compile-time, pass it as the first parameter. See also the performance tip to Annotate values taken from untyped locations.

Examples

julia> @atomize value(p)

julia> @atomize value($1)
Some(1)

julia> @atomize something(value(Int, $2))
2

source

Base.map — Function

map(f, p)

Apply the function f to each atom in p.

Examples

julia> @atomize map(¬, p ∧ q)
¬p ∧ ¬q

julia> @atomize map(atom -> $(something(value(atom)) + 1), $1 ∧ $2)
$(2) ∧ $(3)

source

PAndQ.atoms — Function

atoms(p)

Return an iterator of each atomic proposition contained in p.

Examples

julia> @atomize collect(atoms(p ∧ q))
2-element Vector{PAndQ.Variable}:
 p
 q

source

PAndQ.operators — Function

operators(p)

Return an iterator of each operator contained in p.

Examples

julia> @atomize collect(operators(¬p))
1-element Vector{PAndQ.Interface.Operator{:not}}:
 ¬

julia> @atomize collect(operators(¬p ∧ q))
3-element Vector{PAndQ.Interface.Operator}:
 ∧
 ¬
 𝒾

source

PAndQ.install_atomize_mode — Function

install_atomize_mode(;
    start_key = "\M-a", prompt_text = "atomize> ", prompt_color = :cyan,
kwargs...)

Install the atomize REPL mode, where input implicitly begins with @atomize.

Keyword arguments are passed to ReplMaker.initrepl. The default start keys are pressing both the [Meta] (also known as [Alt]) and [a] keys at the same time. The available prompt_colors are in Base.text_colors.

source

Normalization

PAndQ.normalize — Function

normalize(::Union{typeof(¬), typeof(∧), typeof(∨)}, p)

Convert the given proposition to negation, conjunction, or disjunction normal form depending on whether the first argument is not, and, or or, respectively.

Considering the syntax tree of a normalized proposition, each leaf node is a literal; either an atom or it's negation. Propositions in negation normal form are expanded such that the syntax tree branches only contain the operators and and or. Conjunction and disjunction normal forms are negated normal forms that have been flattened by recursively distributing either the and or or operator over the other. In other words, a collection of literals is a clause and a proposition in conjunctive or disjunctive normal form is a conjunction of disjunctive clauses or a disjunction of conjunctive clauses, respectively.

Conjunction and disjunction, but not negation, normal forms are called canonical. Distributing an operator during conversion may increase the size of the syntax tree exponentially. Therefore, it may be intractable to compute a canonical form for sufficiently large propositions. Instead, use the tseytin transformation to find a proposition in conjunctive normal form which is_equisatisfiable to the given proposition.

Tip

Converting a proposition between conjunction and disjunction normal form is not performant due to the exponential increase in the size of the proposition. It is most performant to apply all operations to propositions and normalizing the resulting proposition once.

Examples

julia> @atomize normalize(∧, ¬(p ∨ q))
(¬p) ∧ (¬q)

julia> @atomize normalize(∨, p ↔ q)
(¬q ∧ ¬p) ∨ (q ∧ p)

source

PAndQ.tseytin — Function

tseytin(p)

Apply the Tseytin transformation to the given proposition.

Using the normalize function to convert a proposition to conjunction normal form may result in an exponentially larger proposition, which can be intractable for sufficiently large propositions. The Tseytin transformation results in a linearly larger proposition that is in conjunction normal form and is_equisatisfiable to the original. However, it contains introduced variables and yields a subset of the solutions to the original proposition.

Examples

julia> is_equisatisfiable(⊤, tseytin(⊤))
true

julia> @atomize is_equisatisfiable(p, tseytin(p))
true

julia> is_equisatisfiable(⊥, tseytin(⊥))
true

source