Repository: whitemech/pylogics (language: python)

Issue:
Prepare for release 0.1.0.alpha0
## Proposed changes

Prepare for release 0.1.0.alpha0

## Fixes

n/a

## Types of changes

What types of changes does your code introduce?
_Put an `x` in the boxes that apply_

- [ ] Bugfix (non-breaking change which fixes an issue)
- [ ] New feature (non-breaking change which adds functionality)
- [ ] Breaking change (fix or feature that would cause existing functionality to not work as expected)

## Checklist

_Put an `x` in the boxes that apply._

- [ ] I have read the [CONTRIBUTING](../blob/master/CONTRIBUTING.md) doc
- [ ] I am making a pull request against the `develop` branch (left side). Also you should start your branch off our `develop`.
- [ ] Lint and unit tests pass locally with my changes
- [ ] I have added tests that prove my fix is effective or that my feature works

## Further comments

n/a


Discussion / hints:

Fix patch:
diff --git a/HISTORY.md b/HISTORY.md
index 56d7b7c..fa2ecec 100644
--- a/HISTORY.md
+++ b/HISTORY.md
@@ -1,3 +1,12 @@
 # History
 
-TODO
+## 0.1.0a0
+
+- Support for Propositional Logic parsing, 
+  syntax representation and parsing.
+- Support for Linear Temporal Logic
+  parsing and syntax representation.
+- Support for Past Linear Temporal Logic
+  parsing and syntax representation.
+- Support for Linear Dynamic Logic 
+  parsing and syntax representation.
diff --git a/README.md b/README.md
index f41346b..42f7cb5 100644
--- a/README.md
+++ b/README.md
@@ -58,7 +58,7 @@ A Python library for logic formalisms representation and manipulation.
 
 To install the package from PyPI:
 ```
-pip install pylogics
+pip install pylogics==0.1.0a0
 ```
 
 ## Tests
diff --git a/docs/grammars.md b/docs/grammars.md
new file mode 100644
index 0000000..c954aa1
--- /dev/null
+++ b/docs/grammars.md
@@ -0,0 +1,254 @@
+
+In this section, all the grammars used 
+by the library are reported here.
+
+## Propositional Logic
+
+The file 
+[`pl.lark`](https://github.com/whitemech/pylogics/blob/main/pylogics/parsers/pl.lark)
+contains the specification of the Lark grammar, and it is reported below:
+
+```lark
+start: propositional_formula
+
+?propositional_formula: prop_equivalence
+?prop_equivalence: prop_implication (EQUIVALENCE prop_implication)*
+?prop_implication: prop_or (IMPLY prop_or)*
+?prop_or: prop_and (OR prop_and)*
+?prop_and: prop_not (AND prop_not)*
+?prop_not: NOT* prop_wrapped
+?prop_wrapped: prop_atom
+            | LSEPARATOR propositional_formula RSEPARATOR
+?prop_atom: atom
+	     | prop_true
+	     | prop_false
+
+atom: SYMBOL_NAME
+prop_true: TRUE
+prop_false: FALSE
+
+LSEPARATOR : "("
+RSEPARATOR : ")"
+EQUIVALENCE : "<->"
+IMPLY : ">>"|"->"
+OR: "||"|"|"
+AND: "&&"|"&"
+NOT: "!"|"~"
+TRUE.2: /(?i:true)/
+FALSE.2: /(?i:false)/
+
+// Symbols cannot contain uppercase letters, because these are reserved
+// Moreover, any word between quotes is a symbol
+SYMBOL_NAME: /[a-z][a-z0-9_]*|"\w+"/
+
+%ignore /\s+/
+```
+
+## Linear Temporal Logic
+
+The Lark grammar for Linear Temporal Logic is defined
+in [`ltl.lark`](https://github.com/whitemech/pylogics/blob/main/pylogics/parsers/ltl.lark),
+and it is reported below:
+
+```lark
+start: ltlf_formula
+
+?ltlf_formula:         ltlf_equivalence
+?ltlf_equivalence:     ltlf_implication (EQUIVALENCE ltlf_implication)*
+?ltlf_implication:     ltlf_or (IMPLY ltlf_or)*
+?ltlf_or:              ltlf_and (OR ltlf_and)*
+?ltlf_and:             ltlf_weak_until (AND ltlf_weak_until)*
+?ltlf_weak_until:      ltlf_until (WEAK_UNTIL ltlf_until)*
+?ltlf_until:           ltlf_release (UNTIL ltlf_release)*
+?ltlf_release:         ltlf_strong_release (RELEASE ltlf_strong_release)*
+?ltlf_strong_release:  ltlf_unaryop (STRONG_RELEASE ltlf_unaryop)*
+
+?ltlf_unaryop:     ltlf_always
+             |     ltlf_eventually
+             |     ltlf_next
+             |     ltlf_weak_next
+             |     ltlf_not
+             |     ltlf_wrapped
+
+?ltlf_always:      ALWAYS ltlf_unaryop
+?ltlf_eventually:  EVENTUALLY ltlf_unaryop
+?ltlf_next:        NEXT ltlf_unaryop
+?ltlf_weak_next:   WEAK_NEXT ltlf_unaryop
+?ltlf_not:         NOT ltlf_unaryop
+?ltlf_wrapped:     ltlf_atom
+             |     LSEPARATOR ltlf_formula RSEPARATOR
+?ltlf_atom:        ltlf_symbol
+          |        ltlf_true
+          |        ltlf_false
+          |        ltlf_last
+
+ltlf_symbol: SYMBOL_NAME
+ltlf_true: prop_true
+ltlf_false: prop_false
+ltlf_last: LAST
+
+UNTIL.2: "U"
+RELEASE.2: "R"
+ALWAYS.2: "G"
+EVENTUALLY.2: "F"
+NEXT.2: "X"
+WEAK_NEXT.2: "N"
+WEAK_UNTIL.2: "W"
+STRONG_RELEASE.2: "M"
+
+END.2: /(?i:end)/
+LAST.2: /(?i:last)/
+
+%ignore /\s+/
+
+%import  .pl.SYMBOL_NAME -> SYMBOL_NAME
+%import  .pl.prop_true -> prop_true
+%import  .pl.prop_false -> prop_false
+%import  .pl.NOT -> NOT
+%import  .pl.OR -> OR
+%import  .pl.AND -> AND
+%import  .pl.EQUIVALENCE -> EQUIVALENCE
+%import  .pl.IMPLY -> IMPLY
+%import  .pl.LSEPARATOR -> LSEPARATOR
+%import  .pl.RSEPARATOR -> RSEPARATOR
+```
+
+## Past Linear Temporal Logic
+
+The Lark grammar for Past Linear Temporal Logic is defined
+in [`pltl.lark`](https://github.com/whitemech/pylogics/blob/main/pylogics/parsers/pltl.lark),
+and it is reported below:
+
+```lark
+start: pltlf_formula
+
+?pltlf_formula:     pltlf_equivalence
+?pltlf_equivalence: pltlf_implication (EQUIVALENCE pltlf_implication)*
+?pltlf_implication: pltlf_or (IMPLY pltlf_or)*
+?pltlf_or:          pltlf_and (OR pltlf_and)*
+?pltlf_and:         pltlf_since (AND pltlf_since)*
+?pltlf_since:       pltlf_unaryop (SINCE pltlf_unaryop)*
+
+?pltlf_unaryop:    pltlf_historically
+             |     pltlf_once
+             |     pltlf_before
+             |     pltlf_not
+             |     pltlf_wrapped
+
+?pltlf_historically: HISTORICALLY pltlf_unaryop
+?pltlf_once:         ONCE pltlf_unaryop
+?pltlf_before:       BEFORE pltlf_unaryop
+?pltlf_not:          NOT pltlf_unaryop
+?pltlf_wrapped:      pltlf_atom
+             |       LSEPARATOR pltlf_formula RSEPARATOR
+?pltlf_atom:       pltlf_symbol
+           |       pltlf_true
+           |       pltlf_false
+           |       pltlf_start
+
+pltlf_symbol: SYMBOL_NAME
+pltlf_true: prop_true
+pltlf_false: prop_false
+pltlf_start: START
+
+// Operators must not be part of a word
+SINCE.2: "S"
+HISTORICALLY.2: "H"
+ONCE.2: "O"
+BEFORE.2: "Y"
+START.2: /(?i:start)/
+
+%ignore /\s+/
+
+%import  .pl.SYMBOL_NAME -> SYMBOL_NAME
+%import  .pl.prop_true -> prop_true
+%import  .pl.prop_false -> prop_false
+%import  .pl.NOT -> NOT
+%import  .pl.OR -> OR
+%import  .pl.AND -> AND
+%import  .pl.EQUIVALENCE -> EQUIVALENCE
+%import  .pl.IMPLY -> IMPLY
+%import  .pl.LSEPARATOR -> LSEPARATOR
+%import  .pl.RSEPARATOR -> RSEPARATOR
+```
+
+## Linear Dynamic Logic
+
+The Lark grammar for Linear Dynamic Logic is defined
+in [`ldl.lark`](https://github.com/whitemech/pylogics/blob/main/pylogics/parsers/ldl.lark),
+and it is reported below:
+
+```lark
+start: ldlf_formula
+
+?ldlf_formula:  ldlf_equivalence
+?ldlf_equivalence: ldlf_implication (EQUIVALENCE ldlf_implication)*
+?ldlf_implication: ldlf_or (IMPLY ldlf_or)*
+?ldlf_or: ldlf_and (OR ldlf_and)*
+?ldlf_and: ldlf_unaryop (AND ldlf_unaryop)*
+
+?ldlf_unaryop:     ldlf_box
+             |     ldlf_diamond
+             |     ldlf_not
+             |     ldlf_wrapped
+?ldlf_box: BOXLSEPARATOR regular_expression BOXRSEPARATOR ldlf_unaryop
+?ldlf_diamond: DIAMONDLSEPARATOR regular_expression DIAMONDRSEPARATOR ldlf_unaryop
+?ldlf_not: NOT ldlf_unaryop
+?ldlf_wrapped:    ldlf_atom
+             |    LSEPARATOR ldlf_formula RSEPARATOR
+?ldlf_atom:   ldlf_tt
+          |   ldlf_ff
+          |   ldlf_last
+          |   ldlf_end
+          |   ldlf_prop_true
+          |   ldlf_prop_false
+          |   ldlf_prop_atom
+
+ldlf_prop_true: TRUE
+ldlf_prop_false: FALSE
+ldlf_prop_atom: SYMBOL_NAME
+
+ldlf_tt: TT
+ldlf_ff: FF
+ldlf_last: LAST
+ldlf_end: END
+
+regular_expression: re_union
+
+?re_union:      re_sequence (UNION re_sequence)*
+?re_sequence:   re_star (SEQ re_star)*
+?re_star:       re_test STAR?
+?re_test:       TEST ldlf_formula
+        |       re_wrapped
+?re_wrapped:    re_propositional
+           |    LSEPARATOR regular_expression RSEPARATOR
+re_propositional: propositional_formula
+
+
+BOXLSEPARATOR: "["
+BOXRSEPARATOR: "]"
+DIAMONDLSEPARATOR: "<"
+DIAMONDRSEPARATOR: ">"
+UNION: "+"
+SEQ: ";"
+TEST: "?"
+STAR: "*"
+TT.2: /(?i:tt)/
+FF.2: /(?i:ff)/
+
+%ignore /\s+/
+
+%import  .pl.propositional_formula
+%import  .pl.TRUE -> TRUE
+%import  .pl.FALSE -> FALSE
+%import  .pl.SYMBOL_NAME -> SYMBOL_NAME
+%import  .pl.EQUIVALENCE -> EQUIVALENCE
+%import  .pl.IMPLY -> IMPLY
+%import  .pl.OR -> OR
+%import  .pl.AND -> AND
+%import  .pl.NOT -> NOT
+%import  .pl.LSEPARATOR -> LSEPARATOR
+%import  .pl.RSEPARATOR -> RSEPARATOR
+%import .ltl.LAST -> LAST
+%import .ltl.END -> END
+```
diff --git a/docs/introduction.md b/docs/introduction.md
new file mode 100644
index 0000000..3e46092
--- /dev/null
+++ b/docs/introduction.md
@@ -0,0 +1,88 @@
+# Introduction
+
+`pylogics` is a Python package 
+to parse and manipulate several
+logic formalisms, with a focus 
+on [temporal logics](https://plato.stanford.edu/entries/logic-temporal/).
+
+> :warning: This library is in early development, and the 
+> API might be broken frequently or may contain bugs :bug:.
+
+> :warning: Docs are not thorough and might be inaccurate.
+> Apologizes.
+
+## Quickstart
+
+For example, consider [Propositional Logic](https://iep.utm.edu/prop-log/).
+The following code allows you to parse a propositional logic formula
+$\phi = (a \wedge b) \vee (c \wedge d)$:
+```python
+from pylogics.parsers import parse_pl
+formula = parse_pl("(a & b) | (c & d)")
+```
+The object referenced by `formula` is an instance
+of `Formula`. Each instance of `Formula` is associated with 
+a certain logic formalism. You can read it
+by accessing the `logic` attribute:
+```
+formlua.logic
+```
+which returns an instance of the Enum class 
+`pylogics.syntax.base.Logic`.
+
+We can evaluate the formula on a propositional interpretation.
+First, import the function `evaluate_pl`:
+```python
+from pylogics.semantics.pl import evaluate_pl
+```
+
+`evaluate_pl` takes in input an instance of
+`Formula`, with `formula.logic` equal to `Logic.PL`,
+and a propositional interpretation $I$ in the form
+of a set of strings or a dictionary from strings to booleans.
+
+- when a set is given, each symbol in the set
+  is considered true; if not, it is considered
+  false.
+- when a dictionary is given, the value
+  of the symbol in the model is determined by
+  the boolean value in the dictionary associated
+  to that key. If the key is not present, it is
+  assumed to be false.
+
+For example, say we want to evaluate 
+the formula over the model $\mathcal{I}_1 = \{a\}$.
+We have $\mathcal{I}_1 \not\models \phi$: 
+```python
+evaluate_pl(formula, {'a'})  # returns False
+```
+
+Now consider $\mathcal{I}_2 = \{a, b\}$.
+We have $\mathcal{I}_2 \models \phi$: 
+```python
+evaluate_pl(formula, {'a', 'b'})  # returns True
+```
+
+Alternatively, we could have written:
+```python
+evaluate_pl(formula, {'a': True, 'b': True, 'c': False})  # returns True
+```
+The value for `d` is assumed to be false, since it is not in the 
+dictionary.
+
+## Other logics
+
+Currently, the package provides support for:
+
+- Linear Temporal Logic (on finite traces) 
+  ([De Giacomo and Vardi, 2013](https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf),
+  [Brafman et al., 2018](http://www.diag.uniroma1.it//~patrizi/docs/papers/BDP@AAAI18.pdf))
+- Past Linear Temporal Logic (on finite traces) 
+  [(De Giacomo et al., 2020)](http://www.dis.uniroma1.it/~degiacom/papers/2020draft/ijcai2020ddfr.pdf)
+- Linear Dynamic Logic (on finite traces)
+  ([De Giacomo and Vardi, 2013](https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf),
+  [Brafman et al., 2018](http://www.diag.uniroma1.it//~patrizi/docs/papers/BDP@AAAI18.pdf))
+
+We consider the variants of these formalisms that also works for empty
+traces; hence (Brafman et al., 2018) is a better reference for the 
+supported logics. More details will be provided in the next sections.
diff --git a/docs/parsing.md b/docs/parsing.md
new file mode 100644
index 0000000..4be5ae0
--- /dev/null
+++ b/docs/parsing.md
@@ -0,0 +1,176 @@
+One of the core features of the library is 
+the support of parsing strings 
+compliant to a certain grammar 
+to handily build formulae.
+
+The parsing functions, one for each logic formalism, 
+can be imported from `pylogics.parsers`, and their
+name is `parse_<id>`, where `<id>` is the 
+identifier of the logic formalism.
+For example, the parsing for propositional logic (`pl`)
+is `parse_pl`, whereas the parsing function
+for Linear Temporal Logic (`ltl`) is `parse_ltl`.
+For a list of the supported logics and their identifier 
+please look at [this page](supported_logics.md).
+
+The library uses [Lark](https://lark-parser.readthedocs.io/en/latest/)
+to generate the parser automatically.
+The grammar files are reported at [this page](grammars.md).
+
+## Symbols
+
+A symbol is determined by the following regular expression:
+
+```
+SYMBOL: [a-z][a-z0-9_]*|"\w+"
+```
+
+That is:
+
+- if between quotes `""`, a symbol can be any 
+  non-empty sequence of word characters: `[a-zA-Z0-9_]+`
+- if not, a symbol must:
+  
+    - have only have lower case characters
+    - have at least one character and start with a non-digit character.
+
+
+## Propositional Logic
+
+Informally, the supported grammar for propositional logic is: 
+```
+pl_formula: pl_formula <-> pl_formula  // equivalence
+          | pl_formula ->  pl_formula  // implication 
+          | pl_formula ||  pl_formula  // disjunction 
+          | pl_formula &&  pl_formula  // conjunction 
+          | !pl_formula                // negation
+          | ( pl_formula )             // brackets 
+          | true                       // boolean constant
+          | false                      // boolean constant
+          | SYMBOL                     // prop. atom
+```
+
+Some examples:
+```python
+from pylogics.parsers import parse_pl
+parse_pl("a")
+parse_pl("b")
+parse_pl("a & b")
+parse_pl("a | b")
+parse_pl("a >> b")
+parse_pl("a <-> b")
+parse_pl("a <-> a")       # returns a
+parse_pl("!(a)")
+parse_pl("true | false")  # returns true
+parse_pl("true & false")  # returns false
+```
+
+## Linear Temporal Logic
+
+Informally, the supported grammar for linear temporal logic is: 
+```
+ltl_formula: ltl_formula <-> ltl_formula  // equivalence
+           | ltl_formula ->  ltl_formula  // implication 
+           | ltl_formula ||  ltl_formula  // disjunction 
+           | ltl_formula &&  ltl_formula  // conjunction 
+           | !ltl_formula                 // negation
+           | ( ltl_formula )              // brackets
+           | ltl_formula U ltl_formula    // until 
+           | ltl_formula R ltl_formula    // release 
+           | ltl_formula W ltl_formula    // weak until 
+           | ltl_formula M ltl_formula    // strong release 
+           | F ltl_formula                // eventually 
+           | G ltl_formula                // always 
+           | X ltl_formula                // next 
+           | N ltl_formula                // weak next 
+           | true                         // boolean constant
+           | false                        // boolean constant
+           | SYMBOL                       // prop. atom
+```
+
+Some examples:
+```python
+from pylogics.parsers import parse_ltl
+parse_ltl("a")
+parse_ltl("b")
+parse_ltl("X(a)")
+parse_ltl("N(b)")
+parse_ltl("F(a)")
+parse_ltl("G(b)")
+parse_ltl("G(a -> b)")
+parse_ltl("a U b")
+parse_ltl("a R b")
+parse_ltl("a W b")
+parse_ltl("a M b")
+```
+
+## Past Linear Temporal Logic
+
+Informally, the supported grammar for past linear temporal logic is: 
+```
+pltl_formula: pltl_formula <-> pltl_formula  // equivalence
+            | pltl_formula ->  pltl_formula  // implication 
+            | pltl_formula ||  pltl_formula  // disjunction 
+            | pltl_formula &&  pltl_formula  // conjunction 
+            | !pltl_formula                  // negation
+            | ( pltl_formula )               // brackets
+            | pltl_formula S pltl_formula    // since 
+            | H pltl_formula                 // historically
+            | O pltl_formula                 // once 
+            | Y pltl_formula                 // before 
+            | true                           // boolean constant
+            | false                          // boolean constant
+            | SYMBOL                         // prop. atom
+```
+
+Some examples:
+```python
+from pylogics.parsers import parse_pltl
+parse_pltl("a")
+parse_pltl("b")
+parse_pltl("Y(a)")
+parse_pltl("O(b)")
+parse_pltl("H(a)")
+parse_pltl("a S b")
+```
+
+## Linear Dynamic Logic
+
+Informally, the supported grammar for linear dynamic logic is
+(note; it is doubly-inductive): 
+```
+ldl_formula: ldl_formula <-> ldl_formula   // equivalence
+           | ldl_formula ->  ldl_formula   // implication 
+           | ldl_formula ||  ldl_formula   // disjunction 
+           | ldl_formula &&  ldl_formula   // conjunction 
+           | !ldl_formula                  // negation
+           | ( ldl_formula )               // brackets
+           | <regex>ldl_formula            // diamond formula
+           | [regex]ldl_formula            // box formula
+           | tt                            // boolean constant
+           | ff                            // boolean constant
+
+regex      : regex + regex                 // union 
+           | regex ; regex                 // sequence 
+           | ?regex                        // test 
+           | regex*                        // star 
+           | pl_formula                    // prop. formula (see above) 
+```
+
+Note: the question mark in the test regular expression 
+is on the left, not on the right. This is done
+to avoid parse conflicts in the parser generation.
+
+Some examples:
+```python
+from pylogics.parsers import parse_ldl
+parse_ldl("tt")
+parse_ldl("ff")
+parse_ldl("<a>tt")
+parse_ldl("[a & b]ff")
+parse_ldl("<a + b>tt")
+parse_ldl("<a ; b><c>tt")
+parse_ldl("<(a ; b)*><c>tt")
+parse_ldl("<true><a>tt")  # Next a
+parse_ldl("<(?<a>tt;true)*>(<b>tt)")  # (a Until b) in LDLf
+```
diff --git a/docs/references.md b/docs/references.md
new file mode 100644
index 0000000..e4cfe8e
--- /dev/null
+++ b/docs/references.md
@@ -0,0 +1,5 @@
+# References
+
+1. G. De Giacomo and M. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI, 2013.
+2. R. Brafman, G. De Giacomo, and F. Patrizi. LTLf/LDLf non-markovian rewards. In AAAI, 2018.
+3. De Giacomo, G., Di Stasio, A., Fuggitti, F., & Rubin, S. (2020). Pure-Past Linear Temporal and Dynamic Logic on Finite Traces. In IJCAI, 2020.
diff --git a/docs/supported_logics.md b/docs/supported_logics.md
new file mode 100644
index 0000000..c60d0e2
--- /dev/null
+++ b/docs/supported_logics.md
@@ -0,0 +1,16 @@
+Each logic formalism is associated
+to a string identifier, to make it
+easier for the user to navigate the APIs.
+
+Follows the table with the supported features
+for each formal language:
+
+| Logics                                   | Identifier  | Parsing            | Syntax             | Semantics          | 
+|------------------------------------------|:-----------:|:------------------:|:------------------:|:------------------:|
+| Propositional Logic                      | `pl`        | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | 
+| Linear Temporal Logic (fin. traces)      | `ltl`       | :heavy_check_mark: | :heavy_check_mark: | :x:                | 
+| Past Linear Temporal Logic (fin. traces) | `pltl`      | :heavy_check_mark: | :heavy_check_mark: | :x:                | 
+| Linear Dynamic Logic (fin. traces)       | `ldl`       | :heavy_check_mark: | :heavy_check_mark: | :x:                | 
+| Past Linear Dynamic Logic (fin. traces)  | `pldl`      | :x:                | :x:                | :x:                | 
+| First-order Logic                        | `fol`       | :x:                | :x:                | :x:                | 
+| Monadic Second-order Logic               | `mso`       | :x:                | :x:                | :x:                | 
diff --git a/docs/syntax.md b/docs/syntax.md
new file mode 100644
index 0000000..b1e6053
--- /dev/null
+++ b/docs/syntax.md
@@ -0,0 +1,110 @@
+The library can also be used through 
+the syntax APIs.
+
+Each class needed to build the syntax tree
+of a formula of a certain logics 
+is in `pylogics.syntax.<id>`,
+where `<id>` is the logic formalism 
+identifier.
+See [this page](supported_logics.md)
+for information about the supported 
+formalisms.
+
+The basic boolean connectives are defined
+in `pylogics.syntax.base`. These are:
+
+- `And`
+- `Or`
+- `Not`
+- `Implies`
+- `Equivalence`
+
+The binary operators take
+in input a sequence of arguments
+instances of a subclass of `Formula`.
+Note that as a precondition the operands.
+must belong to the same logic formalism
+
+E.g. to build $a & b$, one can do: 
+```python
+from pylogics.syntax.pl import Atomic
+a = Atomic("a")
+b = Atomic("b")
+formula = a & b
+```
+
+Now `formula` is an instance of `pylogics.syntax.base.And`.
+For the other operators (except equivalence):
+```
+a | b
+!a
+a >> b
+```
+
+For `true` and `false`, you can use
+`TrueFormula` and `FalseFormula`,
+respectively:
+
+```python
+from pylogics.syntax.base import Logic, TrueFormula, FalseFormula
+true = TrueFormula(logic=Logic.PL)
+false = TrueFormula(logic=Logic.PL)
+```
+
+## Linear Temporal Logic
+
+For LTL, you can use the following classes,
+defined in `pylogics.syntax.ltl`:
+
+- `Atom`, an LTL atom
+- `Next` (unary operator)
+- `WeakNext` (unary operator)
+- `Until` (binary operator)
+- `Release` (binary operator)
+- `WeakUntil` (binary operator)
+- `StrongRelease` (binary operator)
+- `Eventually` (unary operator)
+- `Always` (unary operator)
+
+To combine the above using boolean connectives,
+you can use the classes in `pylogics.syntax.base`
+described above.
+
+## Past Linear Temporal Logic
+
+For PLTL, you can use the following classes,
+defined in `pylogics.syntax.pltl`:
+
+- `Atom`, a PLTL atom
+- `Before` (unary operator)
+- `Since` (binary operator)
+- `Once` (unary operator)
+- `Historically` (unary operator)
+
+To combine the above using boolean connectives,
+you can use the classes in `pylogics.syntax.base`
+described above.
+
+
+## Linear Dynamic Temporal Logic
+
+For LDL, you can use the following classes,
+defined in `pylogics.syntax.ldl`:
+
+- `LDLTrue`, the boolean positive constant `tt`
+- `LDLFalse`, the boolean negative constant `ff`
+- `Diamond(regex, ldlf_formula)`
+- `Box(regex, ldlf_formula)`
+
+To combine the above using boolean connectives,
+you can use the classes in `pylogics.syntax.base`
+described above.
+
+To build regular expressions:
+
+- `Prop(propositional)`, where `propositional` is a 
+  propositional formula (i.e. `propositional.logic` is `Logic.PL`)
+- `Union` (binary operator)
+- `Seq` (binary operator)
+- `Test(ldlf_formula)` (unary operator)
+- `Star(regex)` (unary operator)
diff --git a/mkdocs.yml b/mkdocs.yml
index 17a6c65..0ce3c53 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -4,6 +4,12 @@ repo_url: https://github.com/marcofavorito/pylogics
 
 nav:
 - Home: index.md
+- Introduction: introduction.md
+- Supported Logics: supported_logics.md
+- Parsing: parsing.md
+- Grammars: grammars.md
+- Syntax: syntax.md
+- References: references.md
 
 plugins:
 - search
@@ -14,6 +20,11 @@ theme:
 markdown_extensions:
 - codehilite
 - pymdownx.arithmatex
+- pymdownx.highlight
+- pymdownx.superfences
+- pymdownx.emoji:
+    emoji_index: !!python/name:materialx.emoji.twemoji
+    emoji_generator: !!python/name:materialx.emoji.to_svg
 - markdown_include.include:
     base_path: docs
 
diff --git a/pylogics/__init__.py b/pylogics/__init__.py
index a7cd36b..51e41f4 100644
--- a/pylogics/__init__.py
+++ b/pylogics/__init__.py
@@ -22,4 +22,4 @@
 
 """A Python library for logic formalisms representation and manipulation."""
 
-__version__ = "0.1.0.dev0"
+__version__ = "0.1.0.alpha0"
diff --git a/pylogics/parsers/__init__.py b/pylogics/parsers/__init__.py
index 3d748f9..8340d17 100644
--- a/pylogics/parsers/__init__.py
+++ b/pylogics/parsers/__init__.py
@@ -21,3 +21,8 @@
 #
 
 """This package contains the parsers for the supported logics."""
+
+from .ldl import parse_ldl  # noqa: ignore
+from .ltl import parse_ltl  # noqa: ignore
+from .pl import parse_pl  # noqa: ignore
+from .pltl import parse_pltl  # noqa: ignore
diff --git a/pylogics/parsers/base.py b/pylogics/parsers/base.py
index 0b87cc5..b08da80 100644
--- a/pylogics/parsers/base.py
+++ b/pylogics/parsers/base.py
@@ -99,3 +99,22 @@ def _starred_binaryop(cls, args, formula_type, func_name):
             subformulas = args[::2]
             return formula_type(*subformulas)
         cls._raise_parsing_error(func_name, args)
+
+    @classmethod
+    def _process_unaryop(cls, args, formula_type):
+        """
+        Process a unary operator.
+
+        This parses rules of the form:   rule -> a (OP b)*
+
+        :param args: The parsing Tree.
+        :param formula_type: Constructor of the OP class. It must accept
+            a list of arguments.
+        :return: a Formula.
+        """
+        if len(args) == 1:
+            return args[0]
+        f = args[-1]
+        for _ in args[:-1]:
+            f = formula_type(f)
+        return f
diff --git a/pylogics/parsers/ldl.lark b/pylogics/parsers/ldl.lark
index 44fb642..3b85281 100644
--- a/pylogics/parsers/ldl.lark
+++ b/pylogics/parsers/ldl.lark
@@ -57,16 +57,16 @@ FF.2: /(?i:ff)/
 
 %ignore /\s+/
 
-%import .propositional.propositional_formula
-%import .propositional.TRUE -> TRUE
-%import .propositional.FALSE -> FALSE
-%import .propositional.SYMBOL_NAME -> SYMBOL_NAME
-%import .propositional.EQUIVALENCE -> EQUIVALENCE
-%import .propositional.IMPLY -> IMPLY
-%import .propositional.OR -> OR
-%import .propositional.AND -> AND
-%import .propositional.NOT -> NOT
-%import .propositional.LSEPARATOR -> LSEPARATOR
-%import .propositional.RSEPARATOR -> RSEPARATOR
+%import  .pl.propositional_formula
+%import  .pl.TRUE -> TRUE
+%import  .pl.FALSE -> FALSE
+%import  .pl.SYMBOL_NAME -> SYMBOL_NAME
+%import  .pl.EQUIVALENCE -> EQUIVALENCE
+%import  .pl.IMPLY -> IMPLY
+%import  .pl.OR -> OR
+%import  .pl.AND -> AND
+%import  .pl.NOT -> NOT
+%import  .pl.LSEPARATOR -> LSEPARATOR
+%import  .pl.RSEPARATOR -> RSEPARATOR
 %import .ltl.LAST -> LAST
 %import .ltl.END -> END
diff --git a/pylogics/parsers/ldl.py b/pylogics/parsers/ldl.py
index dd28dd4..049acaf 100644
--- a/pylogics/parsers/ldl.py
+++ b/pylogics/parsers/ldl.py
@@ -24,13 +24,13 @@
 
 from pylogics.exceptions import ParsingError
 from pylogics.parsers.base import AbstractParser, AbstractTransformer
-from pylogics.parsers.propositional import _PLTransformer
+from pylogics.parsers.pl import _PLTransformer
 from pylogics.syntax.base import (
     And,
-    EquivalenceOp,
+    Equivalence,
     FalseFormula,
     Formula,
-    ImpliesOp,
+    Implies,
     Not,
     Or,
     TrueFormula,
@@ -48,15 +48,15 @@
     Test,
     Union,
 )
-from pylogics.syntax.propositional import Atomic
+from pylogics.syntax.pl import Atomic
 
 
 class _LDLTransformer(AbstractTransformer):
     """Transformer for LDL."""
 
     _pl_transformer = _PLTransformer()
-    _pl_imported = ("prop_atom", "propositional_formula")
-    _prefix = "propositional__"
+    _pl_imported = ("pl_atom", "propositional_formula")
+    _prefix = "pl__"
 
     @classmethod
     def start(cls, args):
@@ -70,11 +70,11 @@ def ldlf_formula(cls, args):
 
     @classmethod
     def ldlf_equivalence(cls, args):
-        return cls._starred_binaryop(args, EquivalenceOp, cls.ldlf_equivalence.__name__)
+        return cls._starred_binaryop(args, Equivalence, cls.ldlf_equivalence.__name__)
 
     @classmethod
     def ldlf_implication(cls, args):
-        return cls._starred_binaryop(args, ImpliesOp, cls.ldlf_implication.__name__)
+        return cls._starred_binaryop(args, Implies, cls.ldlf_implication.__name__)
 
     @classmethod
     def ldlf_or(cls, args):
diff --git a/pylogics/parsers/ltl.lark b/pylogics/parsers/ltl.lark
index 92ab964..fd9492e 100644
--- a/pylogics/parsers/ltl.lark
+++ b/pylogics/parsers/ltl.lark
@@ -34,7 +34,6 @@ ltlf_true: prop_true
 ltlf_false: prop_false
 ltlf_last: LAST
 
-// Operators must not be part of a word
 UNTIL.2: "U"
 RELEASE.2: "R"
 ALWAYS.2: "G"
@@ -43,19 +42,19 @@ NEXT.2: "X"
 WEAK_NEXT.2: "N"
 WEAK_UNTIL.2: "W"
 STRONG_RELEASE.2: "M"
+
 END.2: /(?i:end)/
 LAST.2: /(?i:last)/
 
-SYMBOL_NAME: /([A-Za-z][A-Za-z0-9_]*)/
-
 %ignore /\s+/
 
-%import .propositional.prop_true -> prop_true
-%import .propositional.prop_false -> prop_false
-%import .propositional.NOT -> NOT
-%import .propositional.OR -> OR
-%import .propositional.AND -> AND
-%import .propositional.EQUIVALENCE -> EQUIVALENCE
-%import .propositional.IMPLY -> IMPLY
-%import .propositional.LSEPARATOR -> LSEPARATOR
-%import .propositional.RSEPARATOR -> RSEPARATOR
+%import  .pl.SYMBOL_NAME -> SYMBOL_NAME
+%import  .pl.prop_true -> prop_true
+%import  .pl.prop_false -> prop_false
+%import  .pl.NOT -> NOT
+%import  .pl.OR -> OR
+%import  .pl.AND -> AND
+%import  .pl.EQUIVALENCE -> EQUIVALENCE
+%import  .pl.IMPLY -> IMPLY
+%import  .pl.LSEPARATOR -> LSEPARATOR
+%import  .pl.RSEPARATOR -> RSEPARATOR
diff --git a/pylogics/parsers/ltl.py b/pylogics/parsers/ltl.py
index e8ced8b..2368b4f 100644
--- a/pylogics/parsers/ltl.py
+++ b/pylogics/parsers/ltl.py
@@ -25,9 +25,9 @@
 from pylogics.parsers.base import AbstractParser, AbstractTransformer
 from pylogics.syntax.base import (
     And,
-    EquivalenceOp,
+    Equivalence,
     Formula,
-    ImpliesOp,
+    Implies,
     Logic,
     Not,
     Or,
@@ -60,11 +60,11 @@ def ltlf_formula(cls, args):
 
     @classmethod
     def ltlf_equivalence(cls, args):
-        return cls._starred_binaryop(args, EquivalenceOp, cls.ltlf_equivalence.__name__)
+        return cls._starred_binaryop(args, Equivalence, cls.ltlf_equivalence.__name__)
 
     @classmethod
     def ltlf_implication(cls, args):
-        return cls._starred_binaryop(args, ImpliesOp, cls.ltlf_implication.__name__)
+        return cls._starred_binaryop(args, Implies, cls.ltlf_implication.__name__)
 
     @classmethod
     def ltlf_or(cls, args):
@@ -94,48 +94,23 @@ def ltlf_strong_release(cls, args):
 
     @classmethod
     def ltlf_always(cls, args):
-        if len(args) == 1:
-            return args[0]
-        f = args[-1]
-        for _ in args[:-1]:
-            f = Always(f)
-        return f
+        return cls._process_unaryop(args, Always)
 
     @classmethod
     def ltlf_eventually(cls, args):
-        if len(args) == 1:
-            return args[0]
-        f = args[-1]
-        for _ in args[:-1]:
-            f = Eventually(f)
-        return f
+        return cls._process_unaryop(args, Eventually)
 
     @classmethod
     def ltlf_next(cls, args):
-        if len(args) == 1:
-            return args[0]
-        f = args[-1]
-        for _ in args[:-1]:
-            f = Next(f)
-        return f
+        return cls._process_unaryop(args, Next)
 
     @classmethod
     def ltlf_weak_next(cls, args):
-        if len(args) == 1:
-            return args[0]
-        f = args[-1]
-        for _ in args[:-1]:
-            f = WeakNext(f)
-        return f
+        return cls._process_unaryop(args, WeakNext)
 
     @classmethod
     def ltlf_not(cls, args):
-        if len(args) == 1:
-            return args[0]
-        f = args[-1]
-        for _ in args[:-1]:
-            f = Not(f)
-        return f
+        return cls._process_unaryop(args, Not)
 
     @classmethod
     def ltlf_wrapped(cls, args):
diff --git a/pylogics/parsers/propositional.lark b/pylogics/parsers/pl.lark
similarity index 80%
rename from pylogics/parsers/propositional.lark
rename to pylogics/parsers/pl.lark
index e08a4e5..2f05db5 100644
--- a/pylogics/parsers/propositional.lark
+++ b/pylogics/parsers/pl.lark
@@ -23,8 +23,11 @@ IMPLY : ">>"|"->"
 OR: "||"|"|"
 AND: "&&"|"&"
 NOT: "!"|"~"
-SYMBOL_NAME: /([A-Za-z][A-Za-z0-9_]*)/
 TRUE.2: /(?i:true)/
 FALSE.2: /(?i:false)/
 
+// Symbols cannot contain uppercase letters, because these are reserved
+// Moreover, any word between quotes is a symbol
+SYMBOL_NAME: /[a-z][a-z0-9_]*|"\w+"/
+
 %ignore /\s+/
diff --git a/pylogics/parsers/propositional.py b/pylogics/parsers/pl.py
similarity index 85%
rename from pylogics/parsers/propositional.py
rename to pylogics/parsers/pl.py
index 0fcbdb1..65c61d1 100644
--- a/pylogics/parsers/propositional.py
+++ b/pylogics/parsers/pl.py
@@ -25,15 +25,15 @@
 from pylogics.parsers.base import AbstractParser, AbstractTransformer
 from pylogics.syntax.base import (
     And,
-    EquivalenceOp,
+    Equivalence,
     Formula,
-    ImpliesOp,
+    Implies,
     Logic,
     Not,
     Or,
     make_boolean,
 )
-from pylogics.syntax.propositional import Atomic
+from pylogics.syntax.pl import Atomic
 
 
 class _PLTransformer(AbstractTransformer):
@@ -53,11 +53,11 @@ def propositional_formula(cls, args):
     @classmethod
     def prop_equivalence(cls, args):
         """Parse the 'prop_equivalence' tag."""
-        return cls._starred_binaryop(args, EquivalenceOp, cls.prop_equivalence.__name__)
+        return cls._starred_binaryop(args, Equivalence, cls.prop_equivalence.__name__)
 
     @classmethod
     def prop_implication(cls, args):
-        return cls._starred_binaryop(args, ImpliesOp, cls.prop_implication.__name__)
+        return cls._starred_binaryop(args, Implies, cls.prop_implication.__name__)
 
     @classmethod
     def prop_or(cls, args):
@@ -69,12 +69,7 @@ def prop_and(cls, args):
 
     @classmethod
     def prop_not(cls, args):
-        if len(args) == 1:
-            return args[0]
-        f = args[-1]
-        for _ in args[:-1]:
-            f = Not(f)
-        return f
+        return cls._process_unaryop(args, Not)
 
     @classmethod
     def prop_wrapped(cls, args):
@@ -110,13 +105,13 @@ class _PLParser(AbstractParser):
     """Parser for propositional logic."""
 
     transformer_cls = _PLTransformer
-    lark_path = "propositional.lark"
+    lark_path = "pl.lark"
 
 
 __parser = _PLParser()
 
 
-def parse_prop(formula: str) -> Formula:
+def parse_pl(formula: str) -> Formula:
     """
     Parse the propositional formula.
 
diff --git a/pylogics/parsers/pltl.lark b/pylogics/parsers/pltl.lark
new file mode 100644
index 0000000..f06a6ed
--- /dev/null
+++ b/pylogics/parsers/pltl.lark
@@ -0,0 +1,50 @@
+start: pltlf_formula
+
+?pltlf_formula:     pltlf_equivalence
+?pltlf_equivalence: pltlf_implication (EQUIVALENCE pltlf_implication)*
+?pltlf_implication: pltlf_or (IMPLY pltlf_or)*
+?pltlf_or:          pltlf_and (OR pltlf_and)*
+?pltlf_and:         pltlf_since (AND pltlf_since)*
+?pltlf_since:       pltlf_unaryop (SINCE pltlf_unaryop)*
+
+?pltlf_unaryop:    pltlf_historically
+             |     pltlf_once
+             |     pltlf_before
+             |     pltlf_not
+             |     pltlf_wrapped
+
+?pltlf_historically: HISTORICALLY pltlf_unaryop
+?pltlf_once:         ONCE pltlf_unaryop
+?pltlf_before:       BEFORE pltlf_unaryop
+?pltlf_not:          NOT pltlf_unaryop
+?pltlf_wrapped:      pltlf_atom
+             |       LSEPARATOR pltlf_formula RSEPARATOR
+?pltlf_atom:       pltlf_symbol
+           |       pltlf_true
+           |       pltlf_false
+           |       pltlf_start
+
+pltlf_symbol: SYMBOL_NAME
+pltlf_true: prop_true
+pltlf_false: prop_false
+pltlf_start: START
+
+// Operators must not be part of a word
+SINCE.2: "S"
+HISTORICALLY.2: "H"
+ONCE.2: "O"
+BEFORE.2: "Y"
+START.2: /(?i:start)/
+
+%ignore /\s+/
+
+%import  .pl.SYMBOL_NAME -> SYMBOL_NAME
+%import  .pl.prop_true -> prop_true
+%import  .pl.prop_false -> prop_false
+%import  .pl.NOT -> NOT
+%import  .pl.OR -> OR
+%import  .pl.AND -> AND
+%import  .pl.EQUIVALENCE -> EQUIVALENCE
+%import  .pl.IMPLY -> IMPLY
+%import  .pl.LSEPARATOR -> LSEPARATOR
+%import  .pl.RSEPARATOR -> RSEPARATOR
\ No newline at end of file
diff --git a/pylogics/parsers/pltl.py b/pylogics/parsers/pltl.py
new file mode 100644
index 0000000..349ff02
--- /dev/null
+++ b/pylogics/parsers/pltl.py
@@ -0,0 +1,139 @@
+# -*- coding: utf-8 -*-
+#
+# Copyright 2021 WhiteMech
+#
+# ------------------------------
+#
+# This file is part of pylogics.
+#
+# pylogics is free software: you can redistribute it and/or modify
+# it under the terms of the GNU Lesser General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# pylogics is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU Lesser General Public License for more details.
+#
+# You should have received a copy of the GNU Lesser General Public License
+# along with pylogics.  If not, see <https://www.gnu.org/licenses/>.
+#
+
+"""Parser for past linear temporal logic."""
+
+from pylogics.parsers.base import AbstractParser, AbstractTransformer
+from pylogics.syntax.base import (
+    And,
+    Equivalence,
+    Formula,
+    Implies,
+    Logic,
+    Not,
+    Or,
+    make_boolean,
+)
+from pylogics.syntax.pltl import Atomic, Before, Historically, Once, Since, Start
+
+
+class _PLTLTransformer(AbstractTransformer):
+    @classmethod
+    def start(cls, args):
+        assert len(args) == 1
+        return args[0]
+
+    @classmethod
+    def pltlf_formula(cls, args):
+        assert len(args) == 1
+        return args[0]
+
+    @classmethod
+    def pltlf_equivalence(cls, args):
+        return cls._starred_binaryop(args, Equivalence, cls.pltlf_equivalence.__name__)
+
+    @classmethod
+    def pltlf_implication(cls, args):
+        return cls._starred_binaryop(args, Implies, cls.pltlf_implication.__name__)
+
+    @classmethod
+    def pltlf_or(cls, args):
+        return cls._starred_binaryop(args, Or, cls.pltlf_or.__name__)
+
+    @classmethod
+    def pltlf_and(cls, args):
+        return cls._starred_binaryop(args, And, cls.pltlf_and.__name__)
+
+    @classmethod
+    def pltlf_since(cls, args):
+        return cls._starred_binaryop(args, Since, cls.pltlf_since.__name__)
+
+    @classmethod
+    def pltlf_historically(cls, args):
+        return cls._process_unaryop(args, Historically)
+
+    @classmethod
+    def pltlf_once(cls, args):
+        return cls._process_unaryop(args, Once)
+
+    @classmethod
+    def pltlf_before(cls, args):
+        return cls._process_unaryop(args, Before)
+
+    @classmethod
+    def pltlf_not(cls, args):
+        return cls._process_unaryop(args, Not)
+
+    @classmethod
+    def pltlf_wrapped(cls, args):
+        if len(args) == 1:
+            return args[0]
+        if len(args) == 3:
+            _, formula, _ = args
+            return formula
+        cls._raise_parsing_error(cls.pltlf_wrapped.__name__, args)
+
+    @classmethod
+    def pltlf_atom(cls, args):
+        assert len(args) == 1
+        return Atomic(args[0])
+
+    @classmethod
+    def pltlf_true(cls, _args):
+        return make_boolean(True, logic=Logic.PLTL)
+
+    @classmethod
+    def pltlf_false(cls, _args):
+        return make_boolean(False, logic=Logic.PLTL)
+
+    @classmethod
+    def pltlf_start(cls, _args):
+        return Start()
+
+    @classmethod
+    def pltlf_symbol(cls, args):
+        assert len(args) == 1
+        token = args[0]
+        symbol = str(token)
+        return Atomic(symbol)
+
+
+class _PLTLParser(AbstractParser):
+    """Parser for linear temporal logic."""
+
+    transformer_cls = _PLTLTransformer
+    lark_path = "pltl.lark"
+
+
+__parser = _PLTLParser()
+
+
+def parse_pltl(formula: str) -> Formula:
+    """
+    Parse the past linear temporal logic formula.
+
+    This is the main entrypoint for PLTL parsing.
+
+    :param formula: the string representation of the formula.
+    :return: the parsed formula.
+    """
+    return __parser(formula)
diff --git a/pylogics/semantics/base.py b/pylogics/semantics/base.py
index 69cb635..07c4e5f 100644
--- a/pylogics/semantics/base.py
+++ b/pylogics/semantics/base.py
@@ -25,7 +25,7 @@
 from typing import Callable
 
 from pylogics.exceptions import PylogicsError
-from pylogics.syntax.base import And, EquivalenceOp, Formula, ImpliesOp, Not, Or
+from pylogics.syntax.base import And, Equivalence, Formula, Implies, Not, Or
 
 
 @functools.singledispatch
@@ -52,9 +52,9 @@ def not_semantics(formula: Not, fn: Callable[..., bool], *args, **kwargs) -> boo
     return not fn(formula.argument, *args, **kwargs)
 
 
-@base_semantics.register(ImpliesOp)
+@base_semantics.register(Implies)
 def implies_semantics(
-    formula: ImpliesOp, fn: Callable[..., bool], *args, **kwargs
+    formula: Implies, fn: Callable[..., bool], *args, **kwargs
 ) -> bool:
     """
     Evaluate an implication formula.
@@ -78,9 +78,9 @@ def _visitor():
     return any(_visitor())
 
 
-@base_semantics.register(EquivalenceOp)
+@base_semantics.register(Equivalence)
 def equivalence_semantics(
-    formula: EquivalenceOp, fn: Callable[..., bool], *args, **kwargs
+    formula: Equivalence, fn: Callable[..., bool], *args, **kwargs
 ) -> bool:
     """Evaluate an equivalence formula."""
     result = fn(formula.operands[0], *args, **kwargs)
diff --git a/pylogics/semantics/propositional.py b/pylogics/semantics/pl.py
similarity index 80%
rename from pylogics/semantics/propositional.py
rename to pylogics/semantics/pl.py
index e43d3f3..6d2dfae 100644
--- a/pylogics/semantics/propositional.py
+++ b/pylogics/semantics/pl.py
@@ -30,13 +30,13 @@
 from pylogics.semantics.base import base_semantics
 from pylogics.syntax.base import (
     AtomName,
-    BinaryOp,
     FalseFormula,
     Formula,
     TrueFormula,
-    UnaryOp,
+    _BinaryOp,
+    _UnaryOp,
 )
-from pylogics.syntax.propositional import Atomic
+from pylogics.syntax.pl import Atomic
 
 _PropInterpretation = Union[Dict, Set]
 
@@ -65,38 +65,38 @@ def __contains__(self, item: str):
 
 
 @singledispatch
-def evaluate_prop(formula: Formula, _interpretation: _PropInterpretation) -> bool:
+def evaluate_pl(formula: Formula, _interpretation: _PropInterpretation) -> bool:
     """Evaluate a propositional formula against an interpretation."""
     raise PylogicsError(
-        f"formula '{formula}' cannot be processed by {evaluate_prop.__name__}"  # type: ignore
+        f"formula '{formula}' cannot be processed by {evaluate_pl.__name__}"  # type: ignore
     )
 
 
-@evaluate_prop.register(BinaryOp)
-def evaluate_binary_op(formula: BinaryOp, interpretation: _PropInterpretation) -> bool:
+@evaluate_pl.register(_BinaryOp)
+def evaluate_binary_op(formula: _BinaryOp, interpretation: _PropInterpretation) -> bool:
     """Evaluate a propositional formula over a binary operator."""
-    return base_semantics(formula, evaluate_prop, interpretation)
+    return base_semantics(formula, evaluate_pl, interpretation)
 
 
-@evaluate_prop.register(UnaryOp)
-def evaluate_unary_op(formula: UnaryOp, interpretation: _PropInterpretation) -> bool:
+@evaluate_pl.register(_UnaryOp)
+def evaluate_unary_op(formula: _UnaryOp, interpretation: _PropInterpretation) -> bool:
     """Evaluate a propositional formula over a unary operator."""
-    return base_semantics(formula, evaluate_prop, interpretation)
+    return base_semantics(formula, evaluate_pl, interpretation)
 
 
-@evaluate_prop.register(Atomic)
+@evaluate_pl.register(Atomic)
 def evaluate_atomic(formula: Atomic, interpretation: _PropInterpretation) -> bool:
     """Evaluate a propositional formula over an atomic formula."""
     return formula.name in _PropInterpretationWrapper(interpretation)
 
 
-@evaluate_prop.register(TrueFormula)
+@evaluate_pl.register(TrueFormula)
 def evaluate_true(_formula: TrueFormula, _interpretation: _PropInterpretation) -> bool:
     """Evaluate a "true" formula."""
     return True
 
 
-@evaluate_prop.register(FalseFormula)
+@evaluate_pl.register(FalseFormula)
 def evaluate_false(
     _formula: FalseFormula, _interpretation: _PropInterpretation
 ) -> bool:
diff --git a/pylogics/syntax/base.py b/pylogics/syntax/base.py
index eae6d96..ee11298 100644
--- a/pylogics/syntax/base.py
+++ b/pylogics/syntax/base.py
@@ -24,7 +24,7 @@
 import re
 from abc import ABC, abstractmethod
 from enum import Enum
-from typing import Dict, FrozenSet, Optional, Sequence, Union, cast
+from typing import Container, Dict, FrozenSet, Optional, Sequence, Union, cast
 
 from pylogics.exceptions import PylogicsError
 from pylogics.helpers.cache_hash import Hashable
@@ -40,7 +40,7 @@ class Logic(Enum):
     PLTL = "pltl"
     PLDL = "pldl"
     FOL = "fol"
-    SOL = "sol"
+    MSO = "mso"
     RE = "re"
 
 
@@ -112,10 +112,49 @@ def __rshift__(self, other: "Formula") -> "Formula":
         return Or(Not(self), other)
 
 
-class BinaryOp(Formula):
-    """Binary operator."""
+class _MetaOp(_HashConsing):
+    """Metaclass for (binary and unary) operators."""
+
+    def __call__(cls, *operands, **kwargs):
+        """Init the subclass object."""
+        cls._check_not_forbidden_formalism(*operands)
+        return super(_MetaOp, cls).__call__(*operands, **kwargs)
+
+    def _check_not_forbidden_formalism(cls, *operands):
+        """Check operands belong to same formalism."""
+        enforce(len(operands) >= 1, "expected at least one operand.")
+        logic = operands[0].logic
+        allowed = getattr(cls, "ALLOWED_LOGICS", None)
+        forbidden = getattr(cls, "FORBIDDEN_LOGICS", None)
+        if allowed is not None:
+            forbidden = []
+
+        is_logic_allowed = allowed is not None and logic in allowed
+        is_logic_forbidden = forbidden is not None and logic in forbidden
+        if is_logic_allowed and not is_logic_forbidden:
+            raise ValueError(
+                f"error during instantiation of class {cls.__name__}: "
+                f"found operand belonging to logic {logic}, which is forbidden"
+            )
+
+
+class _BinaryOp(Formula):
+    """
+    Binary operator.
+
+    SYMBOL: the symbol to represent this operator in the native string representation.
+    ALLOWED_LOGICS: the collection of allowed formalisms whose formulae can be
+      the arguments of the operator. This has to be set in concrete classes.
+      If None, then the FORBIDDEN_LOGICS field is processed.
+    FORBIDDEN_LOGICS: the collection of formalisms whose formula cannot be
+      the arguments of the operator. This has to be set in concrete classes.
+      If ALLOWED_LOGICS is specified, this field is ignored.
+      If this field is None, then no check is applied.
+    """
 
     SYMBOL: str
+    ALLOWED_LOGICS: Optional[Container[Logic]] = None
+    FORBIDDEN_LOGICS: Optional[Container[Logic]] = None
 
     def __init__(self, *operands: Formula):
         """
@@ -164,10 +203,23 @@ def __eq__(self, other):
         )
 
 
-class UnaryOp(Formula, ABC):
-    """Unary operator."""
+class _UnaryOp(Formula, ABC):
+    """
+    Unary operator.
+
+    SYMBOL: the symbol to represent this operator in the native string representation.
+    ALLOWED_LOGICS: the collection of allowed formalisms whose formulae can be
+      the argument of the operator. This has to be set in concrete classes.
+      If None, then the FORBIDDEN_LOGICS field is processed.
+    FORBIDDEN_LOGICS: the collection of formalisms whose formula cannot be
+      the argument of the operator. This has to be set in concrete classes.
+      If ALLOWED_LOGICS is specified, this field is ignored.
+      If this field is None, then no check is applied.
+    """
 
     SYMBOL: str
+    ALLOWED_LOGICS: Optional[Container[Logic]] = None
+    FORBIDDEN_LOGICS: Optional[Container[Logic]] = None
 
     def __init__(self, arg: Formula):
         """
@@ -298,7 +350,7 @@ def make_boolean(value: bool, logic: Logic) -> Formula:
     return formula_cls(logic=logic)
 
 
-class _MonotoneBinaryOp(_HashConsing):
+class _MonotoneBinaryOp(_MetaOp):
     """
     Metaclass to simplify binary monotone operator instantiations.
 
@@ -375,7 +427,7 @@ def _check_operands_same_logic(mcs, *operands: Formula):
         )
 
 
-class CommutativeBinaryOp(BinaryOp):
+class _CommutativeBinaryOp(_BinaryOp):
     """Commutative binary operator."""
 
     @property
@@ -404,24 +456,27 @@ def __eq__(self, other):
         )
 
 
-class And(CommutativeBinaryOp, metaclass=_MonotoneBinaryOp):
+class And(_CommutativeBinaryOp, metaclass=_MonotoneBinaryOp):
     """And operator."""
 
     _absorbing = False
     SYMBOL = "and"
+    FORBIDDEN_LOGICS = {Logic.RE}
 
 
-class Or(CommutativeBinaryOp, metaclass=_MonotoneBinaryOp):
+class Or(_CommutativeBinaryOp, metaclass=_MonotoneBinaryOp):
     """Or operator."""
 
     _absorbing = True
     SYMBOL = "or"
+    FORBIDDEN_LOGICS = {Logic.RE}
 
 
-class Not(UnaryOp):
+class Not(_UnaryOp):
     """Not operator."""
 
     SYMBOL = "not"
+    FORBIDDEN_LOGICS = {Logic.RE}
 
     def __new__(cls, arg, **kwargs):
         """Instantiate the object."""
@@ -436,7 +491,7 @@ def logic(self) -> Logic:
         return self.argument.logic
 
 
-class _MetaImpliesOp(_HashConsing):
+class _MetaImpliesOp(_MetaOp):
     """
     Metaclass for the imply operator.
 
@@ -473,7 +528,7 @@ def _simplify_operands(*operands):
         return operands
 
 
-class ImpliesOp(BinaryOp, metaclass=_MetaImpliesOp):
+class Implies(_BinaryOp, metaclass=_MetaImpliesOp):
     """
     Implication operator.
 
@@ -481,9 +536,10 @@ class ImpliesOp(BinaryOp, metaclass=_MetaImpliesOp):
     """
 
     SYMBOL = "implies"
+    FORBIDDEN_LOGICS = {Logic.RE}
 
 
-class _MetaEquivalenceOp(_HashConsing):
+class _MetaEquivalenceOp(_MetaOp):
     """
     Metaclass for the equivalence operator.
 
@@ -493,8 +549,7 @@ class _MetaEquivalenceOp(_HashConsing):
     def __call__(cls, *args, **kwargs):
         """Init the subclass object."""
         operands = cls._simplify_operands(*args)
-        if len(args) == 0:
-            raise ValueError("cannot accept zero arguments")
+        enforce(len(args) > 0, "cannot accept zero arguments", ValueError)
         if len(operands) == 1:
             return operands[0]
 
@@ -512,10 +567,11 @@ def _simplify_operands(*operands):
         return operands
 
 
-class EquivalenceOp(CommutativeBinaryOp, metaclass=_MetaEquivalenceOp):
+class Equivalence(_CommutativeBinaryOp, metaclass=_MetaEquivalenceOp):
     """Equivalence operator."""
 
     SYMBOL = "equivalence"
+    FORBIDDEN_LOGICS = {Logic.RE}
 
 
 def ensure_formula(f: Optional[Formula], is_none_true: bool) -> Formula:
@@ -532,7 +588,7 @@ def ensure_formula(f: Optional[Formula], is_none_true: bool) -> Formula:
 class AtomName(RegexConstrainedString):
     """A string that denotes an atomic propositional symbol."""
 
-    REGEX = re.compile(r"[A-Za-z][A-Za-z0-9_]*")
+    REGEX = re.compile(r"[A-Za-z][A-Za-z0-9_]*|\"\w+\"")
 
 
 _AtomNameOrStr = Union[str, AtomName]
diff --git a/pylogics/syntax/ldl.py b/pylogics/syntax/ldl.py
index e37b6b6..7a39b30 100644
--- a/pylogics/syntax/ldl.py
+++ b/pylogics/syntax/ldl.py
@@ -23,16 +23,17 @@
 """Classes for linear dynamic logic."""
 from abc import ABC
 from functools import partial
+from typing import Set
 
 from pylogics.helpers.misc import enforce
 from pylogics.syntax.base import (
-    BinaryOp,
-    CommutativeBinaryOp,
     FalseFormula,
     Formula,
     Logic,
     TrueFormula,
-    UnaryOp,
+    _BinaryOp,
+    _CommutativeBinaryOp,
+    _UnaryOp,
 )
 
 
@@ -98,10 +99,11 @@ def __neg__(self) -> Formula:
         return LDLTrue()
 
 
-class Seq(BinaryOp, _RegularExpression):
+class Seq(_BinaryOp, _RegularExpression):
     """Sequence of regular expressions."""
 
     SYMBOL = "seq"
+    ALLOWED_LOGICS: Set[Logic] = {Logic.RE}
 
     def __post_init__(self):
         """Check consistency after initialization."""
@@ -111,10 +113,11 @@ def __post_init__(self):
         )
 
 
-class Union(CommutativeBinaryOp, _RegularExpression):
+class Union(_CommutativeBinaryOp, _RegularExpression):
     """Union of regular expressions."""
 
     SYMBOL = "union"
+    ALLOWED_LOGICS: Set[Logic] = {Logic.RE}
 
     def __post_init__(self):
         """Check consistency after initialization."""
@@ -124,22 +127,24 @@ def __post_init__(self):
         )
 
 
-class Test(UnaryOp, _RegularExpression):
+class Test(_UnaryOp, _RegularExpression):
     """Test of an LDL formula."""
 
     SYMBOL = "test"
+    ALLOWED_LOGICS: Set[Logic] = {Logic.RE}
 
 
-class Star(UnaryOp, _RegularExpression):
+class Star(_UnaryOp, _RegularExpression):
     """Kleene star of regular expressions."""
 
     SYMBOL = "star"
 
 
-class Prop(UnaryOp, _RegularExpression):
+class Prop(_UnaryOp, _RegularExpression):
     """The propositional regular expression."""
 
     SYMBOL = "prop"
+    ALLOWED_LOGICS: Set[Logic] = {Logic.PL}
 
 
 class _TemporalFormula(_LDL, ABC):
diff --git a/pylogics/syntax/ltl.py b/pylogics/syntax/ltl.py
index faf0ddd..ff12e19 100644
--- a/pylogics/syntax/ltl.py
+++ b/pylogics/syntax/ltl.py
@@ -24,14 +24,13 @@
 from abc import ABC
 from functools import partial
 
-from pylogics.helpers.misc import enforce
 from pylogics.syntax.base import (
     AbstractAtomic,
-    BinaryOp,
     FalseFormula,
     Formula,
     Logic,
-    UnaryOp,
+    _BinaryOp,
+    _UnaryOp,
 )
 
 
@@ -48,25 +47,16 @@ def __hash__(self):
         return super(Formula, self).__hash__()
 
 
-class _LTLUnaryOp(UnaryOp, _LTL):
+class _LTLUnaryOp(_UnaryOp, _LTL):
     """LTL Unary operation."""
 
-    def __post_init__(self):
-        """Check that the argument is of LTL logic."""
-        enforce(
-            self.argument.logic == Logic.LTL, "operand does not belong to LTL logic"
-        )
+    ALLOWED_LOGICS = {Logic.LTL}
 
 
-class _LTLBinaryOp(BinaryOp, _LTL):
+class _LTLBinaryOp(_BinaryOp, _LTL):
     """LTL Unary operation."""
 
-    def __post_init__(self):
-        """Check that the agument is of LTL logic."""
-        enforce(
-            all(op.logic == Logic.LTL for op in self.operands),
-            "operands do not belong to LTL logic",
-        )
+    ALLOWED_LOGICS = {Logic.LTL}
 
 
 class Atomic(AbstractAtomic, _LTL):
diff --git a/pylogics/syntax/propositional.py b/pylogics/syntax/pl.py
similarity index 100%
rename from pylogics/syntax/propositional.py
rename to pylogics/syntax/pl.py
diff --git a/pylogics/syntax/pltl.py b/pylogics/syntax/pltl.py
new file mode 100644
index 0000000..8c3c810
--- /dev/null
+++ b/pylogics/syntax/pltl.py
@@ -0,0 +1,90 @@
+# -*- coding: utf-8 -*-
+#
+# Copyright 2021 WhiteMech
+#
+# ------------------------------
+#
+# This file is part of pylogics.
+#
+# pylogics is free software: you can redistribute it and/or modify
+# it under the terms of the GNU Lesser General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# pylogics is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU Lesser General Public License for more details.
+#
+# You should have received a copy of the GNU Lesser General Public License
+# along with pylogics.  If not, see <https://www.gnu.org/licenses/>.
+#
+
+"""Classes for past linear temporal logic."""
+from abc import ABC
+from functools import partial
+
+from pylogics.syntax.base import (
+    AbstractAtomic,
+    FalseFormula,
+    Formula,
+    Logic,
+    _BinaryOp,
+    _UnaryOp,
+)
+
+
+class _PLTL(Formula, ABC):
+    """Interface for PLTL formulae."""
+
+    @property
+    def logic(self) -> Logic:
+        """Get the logic formalism."""
+        return Logic.PLTL
+
+    def __hash__(self):
+        """Delegate the computation of the hash to the superclass."""
+        return super(Formula, self).__hash__()
+
+
+class _PLTLUnaryOp(_UnaryOp, _PLTL):
+    """PLTL Unary operation."""
+
+    ALLOWED_LOGICS = {Logic.PLTL}
+
+
+class _PLTLBinaryOp(_BinaryOp, _PLTL):
+    """PLTL Unary operation."""
+
+    ALLOWED_LOGICS = {Logic.PLTL}
+
+
+class Atomic(AbstractAtomic, _PLTL):
+    """An atomic proposition of PLTL."""
+
+
+class Before(_PLTLUnaryOp):
+    """The "before" formula in PLTL."""
+
+    SYMBOL = "before"
+
+
+class Since(_PLTLBinaryOp):
+    """The "since" formula in PLTL."""
+
+    SYMBOL = "since"
+
+
+class Once(_PLTLUnaryOp):
+    """The "once" formula in PLTL."""
+
+    SYMBOL = "once"
+
+
+class Historically(_PLTLUnaryOp):
+    """The "historically" formula in PLTL."""
+
+    SYMBOL = "historically"
+
+
+Start = partial(Historically, FalseFormula(logic=Logic.PLTL))
diff --git a/pylogics/utils/to_string.py b/pylogics/utils/to_string.py
index 50a77eb..7fbb058 100644
--- a/pylogics/utils/to_string.py
+++ b/pylogics/utils/to_string.py
@@ -28,10 +28,10 @@
 from pylogics.syntax.base import (
     AbstractAtomic,
     And,
-    EquivalenceOp,
+    Equivalence,
     FalseFormula,
     Formula,
-    ImpliesOp,
+    Implies,
     Not,
     Or,
     TrueFormula,
@@ -57,6 +57,7 @@
     WeakNext,
     WeakUntil,
 )
+from pylogics.syntax.pltl import Before, Historically, Once, Since
 
 
 @functools.singledispatch
@@ -88,14 +89,14 @@ def to_string_not(formula: Not) -> str:
     return f"~({to_string(formula.argument)})"
 
 
-@to_string.register(ImpliesOp)
-def to_string_implies(formula: ImpliesOp) -> str:
+@to_string.register(Implies)
+def to_string_implies(formula: Implies) -> str:
     """Transform an Implies into string."""
     return " -> ".join(_map_operands_to_string(formula.operands))
 
 
-@to_string.register(EquivalenceOp)
-def to_string_equivalence(formula: EquivalenceOp) -> str:
+@to_string.register(Equivalence)
+def to_string_equivalence(formula: Equivalence) -> str:
     """Transform an Equivalence into string."""
     return " <-> ".join(_map_operands_to_string(formula.operands))
 
@@ -166,14 +167,38 @@ def to_string_always(formula: Always) -> str:
     return f"G({to_string(formula.argument)})"
 
 
+@to_string.register(Before)
+def to_string_pltl_before(formula: Before) -> str:
+    """Transform a 'before' formula into string."""
+    return f"Y({to_string(formula.argument)})"
+
+
+@to_string.register(Since)
+def to_string_pltl_since(formula: Since) -> str:
+    """Transform a 'since' formula into string."""
+    return " S ".join(_map_operands_to_string(formula.operands))
+
+
+@to_string.register(Once)
+def to_string_pltl_once(formula: Once) -> str:
+    """Transform a 'once' formula into string."""
+    return f"O({to_string(formula.argument)})"
+
+
+@to_string.register(Historically)
+def to_string_pltl_historically(formula: Historically) -> str:
+    """Transform a 'historically' formula into string."""
+    return f"H({to_string(formula.argument)})"
+
+
 @to_string.register(LDLTrue)
-def to_string_ldl_true(formula: LDLTrue) -> str:
+def to_string_ldl_true(_formula: LDLTrue) -> str:
     """Transform an LDL true into string."""
     return "tt"
 
 
 @to_string.register(LDLFalse)
-def to_string_ldl_false(formula: LDLFalse) -> str:
+def to_string_ldl_false(_formula: LDLFalse) -> str:
     """Transform an LDL false into string."""
     return "ff"
 
diff --git a/pyproject.toml b/pyproject.toml
index 9e91c83..eb186df 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "pylogics"
-version = "0.1.0.dev0"
+version = "0.1.0.alpha0"
 description = "A Python library for logic formalisms representation and manipulation."
 authors = ["MarcoFavorito <marco.favorito@gmail.com>"]
 license = "LGPL-3.0-or-later"
diff --git a/scripts/whitelist.py b/scripts/whitelist.py
index 27b4cb0..d87b4a4 100644
--- a/scripts/whitelist.py
+++ b/scripts/whitelist.py
@@ -27,64 +27,79 @@
 _.start  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:51)
 _.ltlf_formula  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:56)
 _.ltlf_always  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:95)
-_.ltlf_eventually  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:104)
-_.ltlf_next  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:113)
-_.ltlf_weak_next  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:122)
-_.ltlf_not  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:131)
-_.ltlf_atom  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:149)
-_.ltlf_true  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:154)
-_.ltlf_false  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:158)
-_.ltlf_last  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:162)
-_.ltlf_symbol  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:166)
-parse_ltl  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:184)
-_.start  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/propositional.py:42)
-_.propositional_formula  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/propositional.py:47)
-_.prop_not  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/propositional.py:70)
-_.prop_atom  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/propositional.py:88)
-_.prop_true  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/propositional.py:93)
-_.prop_false  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/propositional.py:98)
-_.atom  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/propositional.py:103)
-parse_prop  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/propositional.py:119)
+_.ltlf_eventually  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:99)
+_.ltlf_next  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:103)
+_.ltlf_weak_next  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:107)
+_.ltlf_not  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:111)
+_.ltlf_atom  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:124)
+_.ltlf_true  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:129)
+_.ltlf_false  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:133)
+_.ltlf_last  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:137)
+_.ltlf_symbol  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:141)
+parse_ltl  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/ltl.py:159)
+_.start  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pl.py:42)
+_.propositional_formula  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pl.py:47)
+_.prop_not  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pl.py:70)
+_.prop_atom  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pl.py:83)
+_.prop_true  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pl.py:88)
+_.prop_false  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pl.py:93)
+_.atom  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pl.py:98)
+parse_pl  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pl.py:114)
+_.start  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:40)
+_.pltlf_formula  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:45)
+_.pltlf_historically  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:72)
+_.pltlf_once  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:76)
+_.pltlf_before  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:80)
+_.pltlf_not  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:84)
+_.pltlf_atom  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:97)
+_.pltlf_true  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:102)
+_.pltlf_false  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:106)
+_.pltlf_start  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:110)
+_.pltlf_symbol  # unused method (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:114)
+parse_pltl  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/parsers/pltl.py:132)
 and_semantics  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/base.py:37)
 or_semantics  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/base.py:43)
 not_semantics  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/base.py:49)
 implies_semantics  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/base.py:55)
 equivalence_semantics  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/base.py:81)
-evaluate_binary_op  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/propositional.py:75)
-evaluate_unary_op  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/propositional.py:81)
-evaluate_atomic  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/propositional.py:87)
-evaluate_true  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/propositional.py:93)
-evaluate_false  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/propositional.py:99)
-PLTL  # unused variable (/home/marcofavorito/workfolder/pylogics/pylogics/syntax/base.py:40)
+evaluate_binary_op  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/pl.py:75)
+evaluate_unary_op  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/pl.py:81)
+evaluate_atomic  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/pl.py:87)
+evaluate_true  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/pl.py:93)
+evaluate_false  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/semantics/pl.py:99)
 PLDL  # unused variable (/home/marcofavorito/workfolder/pylogics/pylogics/syntax/base.py:41)
 FOL  # unused variable (/home/marcofavorito/workfolder/pylogics/pylogics/syntax/base.py:42)
-SOL  # unused variable (/home/marcofavorito/workfolder/pylogics/pylogics/syntax/base.py:43)
+MSO  # unused variable (/home/marcofavorito/workfolder/pylogics/pylogics/syntax/base.py:43)
 _.__context  # unused attribute (/home/marcofavorito/workfolder/pylogics/pylogics/syntax/base.py:59)
 reset_cache  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/syntax/base.py:80)
 get_cache_context  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/syntax/base.py:85)
-ensure_formula  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/syntax/base.py:521)
-to_string_and  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:73)
-to_string_or  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:79)
-to_string_not  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:85)
-to_string_implies  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:91)
-to_string_equivalence  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:97)
-to_string_atomic  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:103)
-to_string_true  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:109)
-to_string_false  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:115)
-to_string_next  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:121)
-to_string_weak_next  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:127)
-to_string_until  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:133)
-to_string_weak_until  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:139)
-to_string_release  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:145)
-to_string_strong_release  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:151)
-to_string_eventually  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:157)
-to_string_always  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:163)
-to_string_ldl_true  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:169)
-to_string_ldl_false  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:175)
-to_string_ldl_diamond  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:181)
-to_string_ldl_box  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:187)
-to_string_re_seq  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:193)
-to_string_re_union  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:199)
-to_string_re_star  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:205)
-to_string_re_test  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:211)
-to_string_re_prop  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:217)
+ensure_formula  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/syntax/base.py:577)
+to_string_and  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:74)
+to_string_or  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:80)
+to_string_not  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:86)
+to_string_implies  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:92)
+to_string_equivalence  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:98)
+to_string_atomic  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:104)
+to_string_true  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:110)
+to_string_false  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:116)
+to_string_next  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:122)
+to_string_weak_next  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:128)
+to_string_until  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:134)
+to_string_weak_until  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:140)
+to_string_release  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:146)
+to_string_strong_release  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:152)
+to_string_eventually  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:158)
+to_string_always  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:164)
+to_string_pltl_before  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:170)
+to_string_pltl_since  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:176)
+to_string_pltl_once  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:182)
+to_string_pltl_historically  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:188)
+to_string_ldl_true  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:194)
+to_string_ldl_false  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:200)
+to_string_ldl_diamond  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:206)
+to_string_ldl_box  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:212)
+to_string_re_seq  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:218)
+to_string_re_union  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:224)
+to_string_re_star  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:230)
+to_string_re_test  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:236)
+to_string_re_prop  # unused function (/home/marcofavorito/workfolder/pylogics/pylogics/utils/to_string.py:242)


Test patch:
diff --git a/tests/test_docs.py b/tests/test_docs.py
new file mode 100644
index 0000000..3ab71e8
--- /dev/null
+++ b/tests/test_docs.py
@@ -0,0 +1,77 @@
+# -*- coding: utf-8 -*-
+#
+# Copyright 2021 WhiteMech
+#
+# ------------------------------
+#
+# This file is part of pylogics.
+#
+# pylogics is free software: you can redistribute it and/or modify
+# it under the terms of the GNU Lesser General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# pylogics is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU Lesser General Public License for more details.
+#
+# You should have received a copy of the GNU Lesser General Public License
+# along with pylogics.  If not, see <https://www.gnu.org/licenses/>.
+#
+
+"""Tests for the docs pages."""
+
+from pylogics.parsers import parse_ldl, parse_ltl, parse_pl, parse_pltl
+
+
+def test_pl_parsing():
+    """Test PL parsing."""
+    parse_pl("a")
+    parse_pl("b")
+    parse_pl("a & b")
+    parse_pl("a | b")
+    parse_pl("a >> b")
+    parse_pl("a <-> b")
+    parse_pl("a <-> a")
+    parse_pl("!(a)")
+    parse_pl("true & false")
+    parse_pl("true | false")
+
+
+def test_ltl_parsing():
+    """Test LTL parsing."""
+    parse_ltl("a")
+    parse_ltl("b")
+    parse_ltl("X(a)")
+    parse_ltl("N(b)")
+    parse_ltl("F(a)")
+    parse_ltl("G(b)")
+    parse_ltl("G(a -> b)")
+    parse_ltl("a U b")
+    parse_ltl("a R b")
+    parse_ltl("a W b")
+    parse_ltl("a M b")
+
+
+def test_pltl_parsing():
+    """Test PLTL parsing."""
+    parse_pltl("a")
+    parse_pltl("b")
+    parse_pltl("Y(a)")
+    parse_pltl("O(b)")
+    parse_pltl("H(a)")
+    parse_pltl("a S b")
+
+
+def test_ldl_parsing():
+    """Test LDL parsing."""
+    parse_ldl("tt")
+    parse_ldl("ff")
+    parse_ldl("<a>tt")
+    parse_ldl("[a & b]ff")
+    parse_ldl("<a + b>tt")
+    parse_ldl("<a ; b><c>tt")
+    parse_ldl("<(a ; b)*><c>tt")
+    parse_ldl("<true><a>tt")
+    parse_ldl("<(?<a>tt;true)*>(<b>tt)")
diff --git a/tests/test_propositional.py b/tests/test_pl.py
similarity index 82%
rename from tests/test_propositional.py
rename to tests/test_pl.py
index 3ec8ef4..ec79349 100644
--- a/tests/test_propositional.py
+++ b/tests/test_pl.py
@@ -25,9 +25,9 @@
 from hypothesis.extra.lark import from_lark
 from hypothesis.strategies import booleans, dictionaries, from_regex, one_of, sets
 
-from pylogics.parsers.propositional import __parser as prop_parser
-from pylogics.parsers.propositional import parse_prop
-from pylogics.semantics.propositional import evaluate_prop
+from pylogics.parsers.pl import __parser as prop_parser
+from pylogics.parsers.pl import parse_pl
+from pylogics.semantics.pl import evaluate_pl
 from pylogics.syntax.base import AtomName, Logic, get_cache_context
 from pylogics.utils.to_string import to_string
 from tests.conftest import suppress_health_checks_for_lark
@@ -37,8 +37,8 @@
 @given(from_lark(prop_parser._parser))
 def test_parser(formula):
     """Test parsing is deterministic."""
-    formula_1 = parse_prop(formula)
-    formula_2 = parse_prop(formula)
+    formula_1 = parse_pl(formula)
+    formula_2 = parse_pl(formula)
     assert formula_1 == formula_2
     assert Logic.PL == formula_1.logic == formula_2.logic
 
@@ -47,9 +47,9 @@ def test_parser(formula):
 @given(from_lark(prop_parser._parser))
 def test_to_string(formula):
     """Test that the output of 'to_string' is parsable."""
-    expected_formula = parse_prop(formula)
+    expected_formula = parse_pl(formula)
     formula_str = to_string(expected_formula)
-    actual_formula = parse_prop(formula_str)
+    actual_formula = parse_pl(formula_str)
     assert actual_formula == expected_formula
 
 
@@ -63,22 +63,22 @@ def test_to_string(formula):
 )
 def test_semantics_negation(formula, interpretation):
     """Test that for all models I, (I |= phi) != (I |= ~phi)."""
-    positive_formula = parse_prop(formula)
+    positive_formula = parse_pl(formula)
     negative_formula = ~positive_formula
-    assert evaluate_prop(positive_formula, interpretation) != evaluate_prop(
+    assert evaluate_pl(positive_formula, interpretation) != evaluate_pl(
         negative_formula, interpretation
     )
 
 
 def test_hash_consing():
     """Test that hash consing works as expected."""
-    a1 = parse_prop("A")
+    a1 = parse_pl("a")
     context = get_cache_context()
     assert len(context[a1.logic]) == 1
     assert context[a1.logic][a1] is None
     assert list(context[a1.logic])[0] == a1
 
-    a2 = parse_prop("A")
+    a2 = parse_pl("a")
     assert len(context[a1.logic]) == 1
     assert context[a1.logic][a1] is None
     assert list(context[a1.logic])[0] == a1 == a2
diff --git a/tests/test_pltl.py b/tests/test_pltl.py
new file mode 100644
index 0000000..bb6399c
--- /dev/null
+++ b/tests/test_pltl.py
@@ -0,0 +1,51 @@
+# -*- coding: utf-8 -*-
+#
+# Copyright 2021 WhiteMech
+#
+# ------------------------------
+#
+# This file is part of pylogics.
+#
+# pylogics is free software: you can redistribute it and/or modify
+# it under the terms of the GNU Lesser General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# pylogics is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU Lesser General Public License for more details.
+#
+# You should have received a copy of the GNU Lesser General Public License
+# along with pylogics.  If not, see <https://www.gnu.org/licenses/>.
+#
+
+"""Tests on the pylogics.syntax.pltl module."""
+from hypothesis import given
+from hypothesis.extra.lark import from_lark
+
+from pylogics.parsers.pltl import __parser as pltl_parser
+from pylogics.parsers.pltl import parse_pltl
+from pylogics.syntax.base import Logic
+from pylogics.utils.to_string import to_string
+from tests.conftest import suppress_health_checks_for_lark
+
+
+@suppress_health_checks_for_lark
+@given(from_lark(pltl_parser._parser))
+def test_parser(formula):
+    """Test parsing is deterministic."""
+    formula_1 = parse_pltl(formula)
+    formula_2 = parse_pltl(formula)
+    assert formula_1 == formula_2
+    assert Logic.PLTL == formula_1.logic == formula_2.logic
+
+
+@suppress_health_checks_for_lark
+@given(from_lark(pltl_parser._parser))
+def test_to_string(formula):
+    """Test that the output of 'to_string' is parsable."""
+    expected_formula = parse_pltl(formula)
+    formula_str = to_string(expected_formula)
+    actual_formula = parse_pltl(formula_str)
+    assert actual_formula == expected_formula