If you like propositional logic, then you've come to the right place!
PAndQ.jl is a computer algebra system for propositional logic.
julia> using Pkg: add
julia> add("PAndQ")
julia> using PAndQjulia> ¬⊤
¬⊤
julia> @atomize p ∧ q → $1 ∨ $(1 + 1)
(p ∧ q) → ($(1) ∨ $(2))
julia> @variables p q
2-element Vector{PAndQ.AbstractSyntaxTree}:
p
q
julia> r = p ↔ q
p ↔ q
julia> interpret([p => ⊤], r)
⊤ ↔ q
julia> collect(only(solutions(p ∧ q)[2]))
2-element Vector{Bool}:
1
1
julia> s = normalize(∧, r)
(¬p ∨ q) ∧ (¬q ∨ p)
julia> print_table(p ∧ ¬p, ¬p, r, s)
┌────────┬───┬───┬────┬────────────────────────────┐
│ p ∧ ¬p │ p │ q │ ¬p │ p ↔ q, (¬p ∨ q) ∧ (¬q ∨ p) │
├────────┼───┼───┼────┼────────────────────────────┤
│ ⊥ │ ⊤ │ ⊤ │ ⊥ │ ⊤ │
│ ⊥ │ ⊥ │ ⊤ │ ⊤ │ ⊥ │
├────────┼───┼───┼────┼────────────────────────────┤
│ ⊥ │ ⊤ │ ⊥ │ ⊥ │ ⊥ │
│ ⊥ │ ⊥ │ ⊥ │ ⊤ │ ⊤ │
└────────┴───┴───┴────┴────────────────────────────┘- Operators
- Interface for custom operators
- Propositions
- Syntax and pretty-printing corresponding to written logic
- Simple instantiation
- Custom REPL mode
- Normalization
- Negation, conjunction, and disjunction forms
- Tseytin transformation
- Functor map
- Semantics
- Satisfiability solving
- Logical equivalence
- Strict partial ordering
- Partial interpretation
- Printing
- Diagrams
- Syntax trees
- Truth tables
- Plain text, Markdown, HTML, and LaTeX formats
- DIMACS and LaTeX formats
- Diagrams
- Propositions
- Simplification
- Substitution
- Random generation
- Normal forms
- Algebraic, Blake
- Minimization
- Quine-McCluskey algorithm
- Semantics
- Proofs
- Printing
- Diagrams
- Decision trees
- Circuits
- Typst format
- Parse DIMACS
- Diagrams
- Languages
- Modal logic
- First order logic
- Lambda calculus
- Electronic circuits
- Satisfiability modulo theories
- Julog.jl
- Implements a Prolog-like logic programming language for propositional and first-order logic
- SoleLogics.jl
- Implements several logics and algebras
- Satifsiability.jl
- An interface to satisfiability modulo theory solvers
- Solvers must be installed on the user's system
- LogicCircuits.jl
- Implements propositional logic with support for SIMD and CUDA
- TruthTables.jl
- Implements a macro that prints a truth table
- PAndQ.jl implements a superset of the features in this package
- MathematicalPredicates.jl
- Implements propositional logic
- PAndQ.jl, Julog.jl, and SoleLogics.jl implement a superset of the features in this package
- PicoSat.jl
- An interface to the PicoSAT solver using PicoSAT_jll.jl
- Does not support the Windows operating system
- Z3.jl
- An interface to the Z3 Theorem Prover using z3_jll.jl
- Commits type piracy
These packages are generated by BinaryBuilder.jl.
- Chuffed.jl
- CPLEXCP.jl
- BeeEncoder.jl
- 3+ years since last update