## 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!