How to use

How to use

• Propositional Calculus
• First-order Logic
• REf
• Linear Temporal Logic on Finite Traces
• Linear Dynamic Logic on Finite Traces
• Linear Dynamic Logic on Finite Traces for empty traces

Propositional Calculus

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

First-Order Logic

TODO

REf

TODO

LTLf

TODO

LDLf

TODO

LDLf_FiniteTraces

from pythogic.base.Alphabet import Alphabet
from pythogic.base.Formula import LogicalTrue
from pythogic.base.Symbol import Symbol
from pythogic.base.utils import print_nfa
from pythogic.ldlf_empty_traces.LDLf_EmptyTraces import LDLf_EmptyTraces


a_sym = Symbol("a")
b_sym = Symbol("b")
c_sym = Symbol("c")

alphabet_abc = Alphabet({a_sym, b_sym, c_sym})
ldlf = LDLf_EmptyTraces(alphabet_abc)

tt = LogicalTrue()
nfa = ldlf.to_nfa(tt)
print_nfa(nfa, "000000_alphabet_a_logical_true", "./")