Skip to main content

Python package for deal with logical formulas and formal systems

Project description


.. image::

.. image::

.. image::

.. image::
:alt: Documentation Status

.. image::

.. image::
:alt: MIT License

.. image::
:alt: Codecov coverage

.. image::
:alt: Status: Development

Python package for deal with logical formulas and formal systems.

* Free software: MIT license
* Documentation:


First of all, create symbols and an alphabet

.. code:: python

from pythogic.base.Alphabet import Alphabet
from pythogic.base.Symbol import Symbol

a_sym = Symbol("a")
b_sym = Symbol("b")
c_sym = Symbol("c")
alphabet = Alphabet({a_sym, b_sym, c_sym})
# you can also write:
alphabet = Alphabet.fromStrings({"a", "b", "c"})

Create some formulas:

.. code:: python

from pythogic.base.Formula import AtomicFormula, TrueFormula, FalseFormula, Not, And, Or

# Propositions
a = AtomicFormula(a_sym)
b = AtomicFormula(b_sym)
c = AtomicFormula(c_sym)

# Elementary formulas
not_a = Not(a)
not_a_and_b = And(Not(a), b)
not_a_or_c = Or(not_a, c)
true = TrueFormula()
false = FalseFormula()

Using Propositional Calculus:

.. code:: python

from import PL
from import PLInterpretation

# A dictionary which assign each symbol to a truth value
symbol2truth = {
a_sym: True,
b_sym: False,
c_sym: True

# The propositional interpretation
I = PLInterpretation(alphabet, symbol2truth)

# main class which contains useful methods
PL = PL(alphabet)

PL.truth(a, I) # returns true
PL.truth(b, I) # returns false
PL.truth(c, I) # returns true
PL.truth(not_a, I) # returns false
PL.truth(not_a_and_b, I) # returns false
PL.truth(not_a_or_c, I) # returns true
PL.truth(true, I) # returns true
PL.truth(false, I) # returns false


- Compose logical formula by common syntax rules;
- Implementation of several semantics (FOL Interpretation, finite trace, etc.);
- Support for several logical formal systems: Propositional Logic, First-order Logic, REf, LTLf, LDLf;


This package was created with Cookiecutter_ and the `audreyr/cookiecutter-pypackage`_ project template.

.. _Cookiecutter:
.. _`audreyr/cookiecutter-pypackage`:

Many thanks to PySimpleAutomata_ for the automata support.
.. _PySimpleAutomata:


0.1.0 (2018-02-20)

* First release on PyPI.

0.2.0 (2018-02-23)

* First-Order logic support (Formulas, Interpretations, Assignment, Truth of the formulas).

0.2.1 (2018-02-23)

* Fix on the repo.

0.2.2 (2018-02-25)

* Refactoring of the formulas and formal systems functionalities.
* Implemented LDLf.

0.2.3 (2018-02-25)

* "To negative normal form" procedure for LDLf formulas.

0.2.4 (2018-02-06)

* Support for LDLf for Empty Traces.

0.2.6 (2018-03-09)

* Non-deterministic state automata conversion procedure for LDLf_EmptyTraces formulas.

0.2.7 (2018-03-10)

* Fix bug in delta function for NFA computation from LDLf_EmptyTraces formulas
* Fix bug in rewriting automata for PySimpleAutomata package

0.2.8 (2018-03-10)

* Implemented DFA conversion for NFAs from LDLf_EmptyTraces formulas

0.2.9 (2018-03-16)

* Migrating from PySimpleAutomata to `Pythomata <>`_

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

pythogic-0.2.9.tar.gz (40.7 kB view hashes)

Uploaded source

Built Distribution

pythogic-0.2.9-py3.5.egg (80.4 kB view hashes)

Uploaded 3 5

Supported by

AWS AWS Cloud computing Datadog Datadog Monitoring Facebook / Instagram Facebook / Instagram PSF Sponsor Fastly Fastly CDN Google Google Object Storage and Download Analytics Huawei Huawei PSF Sponsor Microsoft Microsoft PSF Sponsor NVIDIA NVIDIA PSF Sponsor Pingdom Pingdom Monitoring Salesforce Salesforce PSF Sponsor Sentry Sentry Error logging StatusPage StatusPage Status page