PAndQ.jl: A computer algebra system for propositional logic

Package Announcements
, ,
1

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 normalized 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
2

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
3

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
4

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
5

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 :smiley:

1 Like