Skip to content

jakobjpeters/PAndQ.jl

Repository files navigation

Documentation stable Documentation dev

Documentation Continuous Integration

Codecov Dependents

PAndQ.jl

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

Related Packages

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