The Tau language is a language extension of other classical logics (the “base logics”) intended to be a logic whose formulas denote software specifications. A formula specifies a program having at each point of time inputs, outputs, and internal states (memory), which can themselves hold other software specifications, namely a program specification may have as input and output other programs over time. The base logics have to support some structure in order for the Tau language extending them to be well-defined and decidable. In particular, a sufficient condition is that those logics are decidable, propositionally closed (under the classical semantics), and have infinitely many relation or function symbols in their signature. A Tau formula may extend several logics at once.
Domain elements and constants in the Tau language are either natural numbers (N, number sort) or of formula sort F being formulas in the base logics and formulas in the Tau language itself. Formulas are constants and domain elements as well. All formulas are treated only up to logical equivalence. Aside this domain, models contain functions between sequences of domain elements of formula sort. Each sequence itself is a function from the number sort (intuitively time points) to the formula sort. The functions from sequences to sequences model the logical and temporal connection between inputs, outputs, and states. Those functions are restricted to be “time compatible” meaning that no state/output depends at a certain time on some input at some future time.
Overall there are four kinds of quantification aside from the ones already in the base logics: quantification over Tau or base formulas, over Boolean functions and their higher-order counterparts, over natural numbers, and over sequences being functions N->F, where the latter has a special quantifier alternation semantics being the time compatibility condition.
The sort of natural numbers is equipped only with the functions +c, so can only add/subtract from numbers some constant number. The sort of formulas is equipped with Boolean operations and equality (up to logical equivalence), which are sufficient to express e.g. logical entailment.
All mentions of above “sequences” can be replaced with “trees” yielding an even more expressive language. Further the Tau language allows some fixed-point constructs, including LFP, GFP, and PFP.
Given a Tau formula, there are two logical tasks that the backend can perform with them. One is consistency check. It will say whether a Tau formula has a model. Once consistent, a second operation is execution, which is to run the formula as if it was a program. If the formula has more than one model, an arbitrary yet deterministically-chosen program will be executed.
The complexity of the Tau language is hard for ELEMENTARY.
