Skip to content

Latest commit

 

History

History
104 lines (78 loc) · 2.98 KB

README.md

File metadata and controls

104 lines (78 loc) · 2.98 KB
Raw

Mathesis

PyPI Documentation Status PyPI downloads

Mathesis is a human-friendly Python library for computational formal logic (including mathematical, symbolic, philosophical logic), formal semantics, and theorem proving. It is particularly well-suited for:

  • Students learning logic and educators teaching it
  • Researchers in fields like logic, philosophy, linguistics, computer science, and many others

Documentation: https://ozekik.github.io/mathesis/

Installation

pip install mathesis

Key features

  • Interactive theorem proving for humans (proof assistant)
  • Automated reasoning (theorem prover)
  • Define models and check validity of inferences in the models
  • JupyterLab/Jupyter Notebook support
  • Output formulas/proofs in LaTeX
  • Customizable ASCII/Unicode syntax (like A -> B, A → B, A ⊃ B for the conditional)

Supported logics

Propositional logics

Truth Table Tableau Natural Deduction Sequent Calculus
Classical logic ✅ ✅ ✅ ✅
Many-valued logics ✅ - - -
Intuitionistic logic n/a - - ✅

In Progress

  • Modal logics
  • Fuzzy logics
  • Substructural logics
  • Epistemic, doxastic, deontic logics
  • Temporal logics

First-order logics (quantified, predicate logics)

Model Tableau Natural Deduction Sequent Calculus
Classical logic ✅ ✅ - -

In Progress

  • Many-valued logics
  • Modal logics
  • Intuitionistic logic
  • Fuzzy logics
  • Substructural logics
  • Higher-order logics

Development status

Proof theories

  • Tableaux (semantic tableaux, analytic tableaux)
    • Unsigned tableaux
    • Signed tableaux
  • Hilbert systems
    • Hilbert systems
  • Natural deduction
    • Generic natural deduction
    • Gentzen-style natural deduction (Output)
    • Fitch-style natural deduction
  • Sequent calculi (Gentzen-style sequent calculi)
    • Two-sided sequent calculi
    • Hilbert systems in sequent calculus
    • Natural deduction in sequent calculus

Semantics

  • Truth tables
  • Set-theoretic models
  • Possible world semantics (Kripke semantics)
  • Algebraic semantics
  • Game-theoretic semantics
  • Category-theoretic semantics

Internals

Roadmap

  • Add tests
  • Hilbert systems
  • Natural deduction
  • Boolean algebra
  • Type theory
  • Metatheorems
  • Output graphical representations of models
  • Support tptp syntax