Printing
PAndQ.TruthTable
— TypeTruthTable(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 │
├────────┼───┼───┼───────────────┤
│ ⊥ │ ⊤ │ ⊤ │ ⊤ │
│ ⊥ │ ⊥ │ ⊤ │ ⊤ │
├────────┼───┼───┼───────────────┤
│ ⊥ │ ⊤ │ ⊥ │ ⊥ │
│ ⊥ │ ⊥ │ ⊥ │ ⊤ │
└────────┴───┴───┴───────────────┘
PAndQ.formatter
— Functionformatter(T)
Use as the formatters
keyword parameter in print_table
.
T | formatter(T)(true, _, _) | formatter(T)(false, _, _) |
---|---|---|
NullaryOperator | "⊤" | "⊥" |
String | "tautology" | "contradiction" |
Char | "T" | "F" |
Bool | "true" | "false" |
Int | "1" | "0" |
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 │
└───┴───┴───────┘
PAndQ.print_table
— Functionprint_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 │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊤ │
│ ⊥ │ ⊤ │ ⊥ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊥ │
│ ⊥ │ ⊥ │ ⊥ │
└───┴───┴───────┘
PAndQ.print_tree
— Functionprint_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))
∧
├─ ∨
│ ├─ q
│ └─ ¬
│ └─ s
└─ ∨
├─ ¬
│ └─ s
└─ p
PAndQ.print_dimacs
— Functionprint_dimacs(::IO = stdout, p)
Print the DIMACS format of p
.
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
Base.show
— Functionshow(::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, ::Operator)
show(::IO, p)
Print the proposition verbosely.
Examples
julia> @atomize show(stdout, p ∧ q)
and(PAndQ.AbstractSyntaxTree(:p), PAndQ.AbstractSyntaxTree(:q))
julia> and(PAndQ.AbstractSyntaxTree(:p), PAndQ.AbstractSyntaxTree(:q))
p ∧ q