GitHub

Home

Introduction

If you like propositional logic, then you've come to the right place!

PAndQ.jl is a computer algebra system for propositional logic.

Installation

julia> using Pkg: add

julia> add("PAndQ")

julia> using PAndQ

Showcase

julia> ¬⊤
¬⊤

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) │
├────────┼───┼───┼────┼────────────────────────────┤
│ ⊥      │ ⊤ │ ⊤ │ ⊥  │ ⊤                          │
│ ⊥      │ ⊥ │ ⊤ │ ⊤  │ ⊥                          │
├────────┼───┼───┼────┼────────────────────────────┤
│ ⊥      │ ⊤ │ ⊥ │ ⊥  │ ⊥                          │
│ ⊥      │ ⊥ │ ⊥ │ ⊤  │ ⊤                          │
└────────┴───┴───┴────┴────────────────────────────┘

Features

  • 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

Planned

  • Propositions
    • Simplification
    • Substitution
    • Random generation
    • Normal forms
      • Algebraic, Blake
      • Minimization
        • Quine-McCluskey algorithm
  • Semantics
    • Proofs
  • Printing
    • Diagrams
      • Decision trees
      • Circuits
    • Typst format
    • Parse DIMACS
  • Languages
    • Modal logic
    • First order logic
    • Lambda calculus
    • Electronic circuits
    • Satisfiability modulo theories

Logic

  • 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

Wrappers

Binaries

These packages are generated by BinaryBuilder.jl.

Computer Algebra Systems

Constraints

Wrappers