PAndQ.jl

KO | EN

gitlite — search

#python #go #golang #android #machine-learning #nodejs #java #windows #cli #security #pytorch #ios #mcp #openai

(★ 18)

A computer algebra system for propositional logic

PAndQ.jl Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

[![Documentation stable](https://img.shields.io/badge/Documentation-stable-blue.svg)](https://jakobjpeters.github.io/PAndQ.jl/stable/)
[![Documentation dev](https://img.shields.io/badge/Documentation-dev-blue.svg)](https://jakobjpeters.github.io/PAndQ.jl/dev/)

[![Documentation](https://github.com/jakobjpeters/PAndQ.jl/workflows/Documentation/badge.svg)](https://github.com/jakobjpeters/PAndQ.jl/actions/workflows/documentation.yml)
[![Continuous Integration](https://github.com/jakobjpeters/PAndQ.jl/workflows/Continuous%20Integration/badge.svg)](https://github.com/jakobjpeters/PAndQ.jl/actions/workflows/continuous_integration.yml)

[![Codecov](https://codecov.io/gh/jakobjpeters/PAndQ.jl/branch/main/graph/badge.svg?token=XFWU66WSD7)](https://codecov.io/gh/jakobjpeters/PAndQ.jl)
[![Dependents](https://docs.juliahub.com/PAndQ/deps.svg)](https://juliahub.com/ui/Packages/PAndQ/h95uE/0.1.0?page=2)

</div>

# 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
julia> using Pkg: add

julia> add("PAndQ")

julia> using PAndQ
```

## Showcase

```julia
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](https://github.com/ztangent/Julog.jl)
    - Implements a Prolog-like logic programming language for propositional and first-order logic
- [SoleLogics.jl](https://github.com/aclai-lab/SoleLogics.jl)
    - Implements several logics and algebras
- [Satifsiability.jl](https://github.com/elsoroka/Satisfiability.jl)
    - An interface to satisfiability modulo theory solvers
    - Solvers must be installed on the user's system
- [LogicCircuits.jl](https://github.com/Juice-jl/LogicCircuits.jl)
    - Implements propositional logic with support for SIMD and CUDA
- [TruthTables.jl](https://github.com/eliascarv/TruthTables.jl)
    - Implements a macro that prints a truth table
    - PAndQ.jl implements a superset of the features in this package
- [MathematicalPredicates.jl](https://github.com/JuliaReach/MathematicalPredicates.jl)
    - Implements propositional logic
    - PAndQ.jl, Julog.jl, and SoleLogics.jl implement a superset of the features in this package

#### Wrappers

- [PicoSat.jl](https://github.com/sisl/PicoSAT.jl)
    - An interface to the [PicoSAT](https://fmv.jku.at/picosat/) solver using PicoSAT_jll.jl
    - Does not support the Windows operating system
- [Z3.jl](https://github.com/ahumenberger/Z3.jl)
    - An interface to the [Z3 Theorem Prover](https://github.com/Z3Prover/z3) using z3_jll.jl
    - Commits [type piracy](https://docs.julialang.org/en/v1/manual/style-guide/#Avoid-type-piracy)

##### Binaries

These packages are generated by [BinaryBuilder.jl](https://github.com/JuliaPackaging/BinaryBuilder.jl).

- [libpicosat_jll.jl](https://github.com/JuliaBinaryWrappers/libpicosat_jll.jl)
- [PicoSAT_jll.jl](https://github.com/JuliaBinaryWrappers/PicoSAT_jll.jl)
- [z3_jll.jl](https://github.com/JuliaBinaryWrappers/z3_jll.jl)

### Computer Algebra Systems

- [Metatheory.jl](https://github.com/JuliaSymbolics/Metatheory.jl)
- [SymbolicUtils.jl](https://github.com/JuliaSymbolics/SymbolicUtils.jl)
- [Symbolics.jl](https://github.com/JuliaSymbolics/Symbolics.jl)
- [Oscar.jl](https://github.com/oscar-system/Oscar.jl)
- [Catlab.jl](https://github.com/AlgebraicJulia/Catlab.jl)

### Constraints

- [JuMP.jl](https://github.com/jump-dev/JuMP.jl)
- [ConstraintSolver.jl](https://github.com/Wikunia/ConstraintSolver.jl)

#### Wrappers

- [Chuffed.jl](https://github.com/JuliaConstraints/Chuffed.jl)
- [CPLEXCP.jl](https://github.com/JuliaConstraints/CPLEXCP.jl)
- [BeeEncoder.jl](https://github.com/newptcai/BeeEncoder.jl)
    - 3+ years since last update

PAndQ.jl

PAndQ.jl Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

PAndQ.jl

PAndQ.jl Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README