Skip to content
This repository has been archived by the owner on Apr 10, 2019. It is now read-only.
/ pythogic Public archive

A Python package for deal with logical formulas and formal systems (e.g. FOL)

License

Notifications You must be signed in to change notification settings

marcofavorito/pythogic

Repository files navigation

Pythogic

DEPRECATED

The development and the support are temporarily suspended.

Documentation Status https://coveralls.io/repos/github/MarcoFavorito/pythogic/badge.svg?branch=master&service=github MIT License Codecov coverage Status: Development

Python package for deal with logical formulas and formal systems.

Usage

First of all, create symbols and an alphabet

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:

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:

from pythogic.pl.PL import PL
from pythogic.pl.semantics.PLInterpretation 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

Features

  • 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;

Credits

This package was created with Cookiecutter and the audreyr/cookiecutter-pypackage project template.

Many thanks to PySimpleAutomata_ for the automata support. .. _PySimpleAutomata: https://github.com/Oneiroe/PySimpleAutomata