Printing

TruthTable(ps)

Construct a truth table for the given propositions.

The header is a sequence of propositions. The body is a matrix where the rows are interpretations of each proposition in the header.

Propositions logically equivalent to a truth value will be grouped on the left, followed by those equivalent to an atomic proposition, and then by all other propositions. Logically equivalent propositions will be grouped together. Propositions that have the same text representation will only be shown once.

Examples

julia> TruthTable([⊤])
┌───┐
│ ⊤ │
├───┤
│ ⊤ │
└───┘

julia> @atomize TruthTable([¬p])
┌───┬────┐
│ p │ ¬p │
├───┼────┤
│ ⊤ │ ⊥  │
│ ⊥ │ ⊤  │
└───┴────┘

julia> @atomize TruthTable([p ∧ ¬p, p → q, ¬p ∨ q])
┌────────┬───┬───┬───────────────┐
│ p ∧ ¬p │ p │ q │ p → q, ¬p ∨ q │
├────────┼───┼───┼───────────────┤
│ ⊥      │ ⊤ │ ⊤ │ ⊤             │
│ ⊥      │ ⊥ │ ⊤ │ ⊤             │
├────────┼───┼───┼───────────────┤
│ ⊥      │ ⊤ │ ⊥ │ ⊥             │
│ ⊥      │ ⊥ │ ⊥ │ ⊤             │
└────────┴───┴───┴───────────────┘

formatter(T)

Use as the formatters keyword parameter in print_table.

See also Nullary Operators.

Examples

julia> @atomize print_table(p ∧ q; formatters = formatter(Bool))
┌───────┬───────┬───────┐
│ p     │ q     │ p ∧ q │
├───────┼───────┼───────┤
│ true  │ true  │ true  │
│ false │ true  │ false │
├───────┼───────┼───────┤
│ true  │ false │ false │
│ false │ false │ false │
└───────┴───────┴───────┘

julia> @atomize print_table(p ∧ q; formatters = formatter(Int))
┌───┬───┬───────┐
│ p │ q │ p ∧ q │
├───┼───┼───────┤
│ 1 │ 1 │ 1     │
│ 0 │ 1 │ 0     │
├───┼───┼───────┤
│ 1 │ 0 │ 0     │
│ 0 │ 0 │ 0     │
└───┴───┴───────┘

print_table(::IO = stdout, xs...; kwargs...)

Print a TruthTable.

The parameters can be a TruthTable, iterable of propositions, or sequence of propositions.

Keyword parameters are passed to PrettyTables.pretty_table.

Examples

julia> print_table(TruthTable([⊤]))
┌───┐
│ ⊤ │
├───┤
│ ⊤ │
└───┘

julia> @atomize print_table([p])
┌───┐
│ p │
├───┤
│ ⊤ │
│ ⊥ │
└───┘

julia> @atomize print_table(p ∧ q)
┌───┬───┬───────┐
│ p │ q │ p ∧ q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊤     │
│ ⊥ │ ⊤ │ ⊥     │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊥     │
│ ⊥ │ ⊥ │ ⊥     │
└───┴───┴───────┘

print_tree(::IO = stdout, p; kwargs...)

Print a tree diagram of the given proposition.

Keyword parameters are passed to AbstractTrees.print_tree.

julia> @atomize print_tree(p ∧ q ∨ ¬s)
∨
├─ ∧
│  ├─ 𝒾
│  │  └─ p
│  └─ 𝒾
│     └─ q
└─ ¬
   └─ s

julia> @atomize print_tree(normalize(∧, p ∧ q ∨ ¬s))
∧
├─ ∨
│  ├─ ¬
│  │  └─ s
│  └─ 𝒾
│     └─ q
└─ ∨
   ├─ ¬
   │  └─ s
   └─ 𝒾
      └─ p

print_dimacs(io = stdout, p)

Print the DIMACS format of p.

The io can be an IO or file path String to write to.

Examples

julia> @atomize print_dimacs(p ∧ q)
p cnf 2 2
1 0
2 0

julia> @atomize print_dimacs(p ↔ q)
p cnf 2 2
1 -2 0
-1 2 0

show(::IO, ::MIME"text/plain", ::Operator)

Print the operator's symbol.

Examples

julia> show(stdout, "text/plain", ⊤)
⊤

julia> show(stdout, "text/plain", ¬)
¬

julia> show(stdout, "text/plain", ∧)
∧

show(::IO, ::MIME"text/plain", p)

Print the proposition in logical syntax format.

The value of a constant is shown with an IOContext whose :compact and :limit keys are individually set to true if they have not already been set.

Examples

julia> @atomize show(stdout, "text/plain", p ∧ q)
p ∧ q

julia> @atomize show(stdout, "text/plain", (p ∨ q) ∧ (r ∨ s))
(p ∨ q) ∧ (r ∨ s)

show(::IO, ::MIME"text/plain", ::TruthTable)

Print the TruthTable's default format.

Examples

julia> @atomize show(stdout, "text/plain", TruthTable([p ∧ q]))
┌───┬───┬───────┐
│ p │ q │ p ∧ q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊤     │
│ ⊥ │ ⊤ │ ⊥     │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊥     │
│ ⊥ │ ⊥ │ ⊥     │
└───┴───┴───────┘

show(::IO, p)

Print the proposition verbosely.

Examples

julia> @atomize show(stdout, p ∧ q)
and(identical(PAndQ.Variable(:p)), identical(PAndQ.Variable(:q)))

julia> and(identical(PAndQ.Variable(:p)), identical(PAndQ.Variable(:q)))
p ∧ q