The user can define propositional logic formula consisting of logical operators and atomic propositions.

State formula:

state_formula:	atomic_proposition
	| un_operator state_formula
	| state_formula bin_operator state_formula
	| ( state_formula )

Logical operators:

un_operator:	!                      (negation)
	| -                    (negation)
bin_operator:	&                   (conjunction)
	| *                     (conjunction)
	| |                    (disjunction)
	| +                    (disjunction)
	| =>                 (implication)

Atomic propositions:

The atomic propositions can be different for the input languages.
See APNN, B(PN)^2, CFA, PEP, SENIL.