| EH2000 |
This class relies on EH2000 to simplify
a QPTL formula if it has no quantification. |
| QPTL |
This class provides common methods for QPTL formulae.
|
| QPTLAlways |
This class represents QPTL formulae in "[] f" form.
|
| QPTLAnd |
This class represents QPTL formulae in "f ∧ g" form.
|
| QPTLAtomic |
This class represents the atomic propositions in QPTL.
|
| QPTLBackto |
This class represents QPTL formulae in "f B g" form.
|
| QPTLBefore |
This class represents QPTL formulae in (~) f" form.
|
| QPTLBinary |
This class represents QPTL formulae formed by a binary operator, for example
"f U g", "f R g", "f S g", "f B g", "f T g", "f --> g", or
"f <--> g".
|
| QPTLCreator |
This is a creator that can create a string representing a QPTL formula.
|
| QPTLEquivalence |
This class represents QPTL formulae in "f <--> g" form.
|
| QPTLExists |
This class represents QPTL formulae in "E t : f(t)" form.
|
| QPTLForall |
This class represents QPTL formulae in "A t : f(t)" form.
|
| QPTLFormula |
A QPTLFormula object holds a string that is supposed to be a QPTL
formula.
|
| QPTLImplication |
This class represents QPTL formulae in "f --> g" form.
|
| QPTLNegation |
This class represents QPTL formulae in "~ f" form.
|
| QPTLNext |
This class represents QPTL formulae in "() f" form.
|
| QPTLOnce |
This class represents QPTL formulae in "<-> f" form.
|
| QPTLOr |
This class represents QPTL formulae in "f1 ∨ g" form.
|
| QPTLParenthesis |
This class represents a QPTL formula enclosed by parentheses.
|
| QPTLParser |
A QPTLParser can parse a string into a QPTL object.
|
| QPTLPastEvaluator |
This class provides a rewriter that can evaluate past formulae at the initial
position.
|
| QPTLPastFutureSeparator |
This class provides a separation of past and future operators for QPTL
formulae that are convertible to prenex normal form.
|
| QPTLPrevious |
This class represents QPTL formulae in "(-) f" form.
|
| QPTLQuantification |
This class represents QPTL formulae with an out-most quantifier.
|
| QPTLRelease |
This class represents QPTL formulae in "f R g" form.
|
| QPTLRewritePattern |
A QPTLRewritePattern object contains several syntactical rewrite
patterns represented as a map from the pattern to the replacement.
|
| QPTLSimplifier |
This class provides a rewriter for simplifying QPTL formulae.
|
| QPTLSince |
This class represents QPTL formulae in "f S g" form.
|
| QPTLSofar |
This class represents QPTL formula in "[-] f" form.
|
| QPTLSometime |
This class represents QPTL formulae in "<> f" form.
|
| QPTLTemporalHierarchy |
This class provides methods for checking syntactically if a QPTL formula is a
standard κ-formula based on [Edward Y.
|
| QPTLTrigger |
This class represents QPTL formulae in "f T g" form.
|
| QPTLUnary |
This class represents QPTL formulae obtained by applying a unary operator to
a QPTL formula, for example, "~ f", "() f", "<> f", "[] f", "(-) f",
"(~) f", "<-> f", and "[-] f".
|
| QPTLUnifier |
A QPTLUnifier can perform unification on two QPTL formulae: source
and target.
|
| QPTLUnless |
This class represents QPTL formulae in "f W g" form.
|
| QPTLUntil |
This class represents QPTL formulae in "f U g" form.
|
| QPTLUtil |
This class provides some useful methods for processing QPTL formulae.
|
| RandomQPTL |
This class provides a generator of random QPTL formulae.
|
| RandomQPTLFormula |
This class provides a generator of random QPTL formulae.
|