# PAndQ.jl: A computer algebra system for propositional logic

## Introduction

Hi everyone! Iβm excited to introduce PAndQ.jl. It was registered unannounced last year, so I wanted to write an official announcement following the new v0.3.0 release.

PAndQ.jl enables you to create, manipulate, solve, and print symbolic propositions with ease. The backend libpicosat_jll.jl solver efficiently handles larger propositions, as demonstrated in this Sudoku tutorial. This package stands out for its polished API and extensive features, making it the top choice for propositional logic in Julia.

## Features

There are 16 built-in operators, each with a name and symbolic alias. If thatβs not enough, create your own operators with custom semantics and printing.

``````julia> not(and(tautology, contradiction))
Β¬(β€ β§ β₯)

julia> Β¬(β€ β§ β₯)
Β¬(β€ β§ β₯)
``````

Itβs easy to instantiate atomic propositions as variables (such as `p` and `q`) and constants (such as `1` and `"two"`). The macro `@variables` defines variables while `@atomize` instantiates variables and constants inline. Use `install_atomize_mode` in the REPL to implicitly begin each line with `@atomize`.

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

julia> p β§ q
p β§ q

julia> @atomize \$1 β \$"two"
\$(1) β \$("two")
``````

Propositions can be `normalize`d to negation, disjunction, and conjunction normal forms. This may result in exponentially larger propositions, which you can avoid by applying the `tseytin` transformation.

``````julia> normalize(β§, p β q)
(Β¬p β¨ q) β§ (Β¬q β¨ p)

julia> normalize(β¨, p β q)
(Β¬q β§ Β¬p) β¨ (q β§ p)
``````

You can partially `interpret` propositions by substituting their atoms with other propositions. The `solutions` to a proposition are the `valuations` that result in a `true` interpretation. There are also several predicate functions to provide more specific information relating to satisfiability.

``````julia> interpret(p => β€, p β§ q)
β€ β§ q

julia> collect(only(solutions(p β§ q)))
2-element Vector{Pair{PAndQ.Variable, Bool}}:
PAndQ.Variable(:p) => 1
PAndQ.Variable(:q) => 1

julia> is_satisfiable(p β§ Β¬p)
false
``````

Propositions can be compared by logical equivalence and a strict partial order.

``````julia> (p β q) == (Β¬p β¨ q)
true

julia> β₯ < p < β€
true
``````

There are several methods to print propositions. Print truth tables with the PrettyTables.jl backend, enabling extensive customization including Markdown, HTML, and LaTeX formatting. The LaTeX format requires loading the Latexify.jl extension, which also enables you to `latexify` propositions. Finally, propositions can be printed as an abstract syntax tree and in DIMACS format.

``````julia> print_table(Β¬p, p β§ q)
βββββ¬ββββ¬βββββ¬ββββββββ
β p β q β Β¬p β p β§ q β
βββββΌββββΌβββββΌββββββββ€
β β€ β β€ β β₯  β β€     β
β β₯ β β€ β β€  β β₯     β
βββββΌββββΌβββββΌββββββββ€
β β€ β β₯ β β₯  β β₯     β
β β₯ β β₯ β β€  β β₯     β
βββββ΄ββββ΄βββββ΄ββββββββ

julia> print_dimacs(p β q)
p cnf 2 1
-1 2 0
``````

## Conclusion

There are many new features and performance optimizations to come, so watch for updates! Please reach out with comments, questions, suggestions, issues, and contributions. Iβm active in the Humans of Julia Discord and the Julia Slack. This package is incredibly fun to develop, and I hope you enjoy using it.

Thank you for taking the time to check out PAndQ.jl!

22 Likes

I am curious, can I use PAndQ.jl to:

1. Start with a truth table and automatically derive a boolean expression for the truth table?
2. Simplify a large boolean expression into a smaller boolean expression?
1 Like

Great questions!

### 1

Yes you can! I can interpret your question in two different ways, so please let me know if one of them is satisfactory or if I am misunderstanding your question. I admit that it took a bit of time to construct these methods, and it would be much easier if they were features in their own right. Would you want such features and do you have any use cases or motivations for them? βI just want thisβ is excellent motivation!

Given the truth table:

``````βββββ¬ββββ¬ββββ¬ββββ
β p β q β r β s β
βββββΌββββΌββββΌββββ€
β β€ β β€ β β₯ β β€ β
β β₯ β β€ β β€ β β₯ β
βββββΌββββΌββββΌββββ€
β β€ β β₯ β β₯ β β₯ β
β β₯ β β₯ β β€ β β₯ β
βββββ΄ββββ΄ββββ΄ββββ
``````

#### First method

Weβre looking for a proposition whose solutions are the same as the interpretations (rows) in the truth table. The function `rows_to_interpretations` returns a collection where each element is an interpretation; a map from the propositions to their truth values, as is implicit in the truth table.

``````julia> @variables p q r s;

julia> rows_to_interpretations(ps, rows) =
map(truth_values -> Pair.(ps, truth_values), rows);

julia> ps = [p, q, r, s];

julia> rows = eachrow([β€ β€ β₯ β€; β₯ β€ β€ β₯; β€ β₯ β₯ β₯; β₯ β₯ β€ β₯]);
``````

Then, I create the target proposition `x` with the fold function, which is a little bit magic but works like `mapreduce` in this case. Each pair `(p => t)` is asserted to be equivalent via bi-directional implication `β`. The pairs in each interpretation are joined by conjunction `β§`, and then each interpretation is joined by disjunction `β¨`.

``````julia> interpretations = rows_to_interpretations(ps, rows);

julia> x = fold(interpretation -> fold(splat(β), (β§) => interpretation), (β¨) => interpretations)
((((((p β β€) β§ (q β β€)) β§ (r β β₯)) β§ (s β β€)) β¨ ((((p β β₯) β§ (q β β€)) β§ (r β β€)) β§ (s β β₯))) β¨ ((((p β β€) β§ (q β β₯)) β§ (r β β₯)) β§ (s β β₯))) β¨ ((((p β β₯) β§ (q β β₯)) β§ (r β β€)) β§ (s β β₯))
``````

Finally, I show that the original set of interpretations is equivalent to the set of interpretations given by the `solutions` of `x`.

``````julia> _solutions = rows_to_interpretations(ps, map(row -> Bool.(row), rows));

julia> solution_set(_solutions) = Set(Set.(_solutions));

julia> solution_set(solutions(x)) == solution_set(_solutions)
true
``````

#### Second method

Assume that we know `p` and `q` are atomic and that we are looking for `r` and `s`. The `construct` function accepts a collection of atomic propositions `ps`, where `rows` are their corresponding truth values. Construct the interpretations with `rows_to_interpretations`, then assert that each interpretation implies the corresponding `target` truth value.

``````julia> function construct(ps, rows, target)
length(ps) ^ 2 == size(rows, 1) == length(target) || throw(DimensionMismatch())
interpretations = rows_to_interpretations(ps, rows)
fold((β§) => zip(interpretations, target)) do valuation, t
fold(splat(β), (β§) => valuation) β t
end;
``````

Given the interpretations and target truth values, the resulting propositions `r` and `s` reconstruct the original truth table.

``````julia> ps = [p, q];

julia> rows = eachrow([β€ β€; β₯ β€; β€ β₯; β₯ β₯]);

julia> targets = ([β₯, β€, β₯, β€], [β€, β₯, β₯, β₯]);

julia> r, s = map(targets) do target
normalize(β§, construct(ps, rows, target))
end;

julia> print_table(Β¬p, p β§ q, r, s)
βββββ¬ββββ¬βββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββββββββββ
β p β q β Β¬p, (Β¬q β¨ Β¬p) β§ (q β¨ Β¬p) β p β§ q, (q β¨ p) β§ ((q β¨ Β¬p) β§ (p β¨ Β¬q)) β
βββββΌββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββ€
β β€ β β€ β β₯                        β β€                                      β
β β₯ β β€ β β€                        β β₯                                      β
βββββΌββββΌβββββββββββββββββββββββββββΌβββββββββββββββββββββββββββββββββββββββββ€
β β€ β β₯ β β₯                        β β₯                                      β
β β₯ β β₯ β β€                        β β₯                                      β
βββββ΄ββββ΄βββββββββββββββββββββββββββ΄βββββββββββββββββββββββββββββββββββββββββ
``````

### 2

Not yet, but simplification is in the planned features. I have done some initial research into what this will look like, and am currently thinking that I will re-implement the semantics with Metatheory.jl. It will take some time, perhaps in v0.5 or v0.6? Iβm open to ideas!

2 Likes

Interesting. Thank you for making this package.

One thing I was wondering is whether it can check whether a conclusion is valid. For example, p β q, p, therefore q. It would be easy to glean that from a truth table, but it might be more difficult with more complex expressions.

1 Like

Youβre welcome! I havenβt ventured very far into proofs, although those are also in the list of planned features. However, I think that such functionality can be defined like so (please correct me if Iβm getting it wrong!):

``````julia> deduce(premises, conclusion) =
is_tautology(β(premises) β conclusion);

julia> deduce([p, p β q], q)
true
``````

Note that `conjunction` (`β`) is a fold of `and` (`β§`).

If this works as I think it does, it could very well be exported in a future release! Thank you for the idea

1 Like