Информационная система "Конференции"

Abstracts

Applications of logic in computer science

In [1] M.Fitting has proposed the idea of extension of propositional modal logics by predicate lambda-abstraction. Take any propositional modal logic L and add relation symbols (including, possibly, equality), flexible constants and the operator of predicate abstraction, but no quantifiers. The result will be a logic $L_lambda(=)$, which is in a sense, intermediate between propositional and first-order. It is proved in [1] that such extension of S5 is undecidable, and for many other classical modal logics L their extensions $L_{lambda(=)}$ are still decidable.

In [2] we have started the study of $LTL_lambda(=)$, the linear time temporal logic, extended by lambda-abstraction. We have demonstrated that $LTL_lambda(=)$ can be used for specification of computational processes (agents) using resources. Despite being very restricted fragment of the first-order temporal logic the logic $LTL_lambda=$ (with equality) has turned out to be not recursively axiomatizable [2]. This is proved by modelling the computations of two-counter Minsky machines in the logic.

Here we present further results on axiomatizability and expressive power of (fragments of) $LTL_lambda=$.

Theorem 1. $LTL_{lambda}$, that is a linear temporal logic with $lambda$-abstraction and without equality is not recursively axiomatizable.

The proof is done by reduction of the validity problem for first-order (non-temporal) logic over finite domains to the validity problem for $LTL_{lambda}$.

Theorem 2. $LTL_{lambda(=)}$ is strictly less expressive than first-order linear temporal logic and strictly more expressive than propositional linear temporal logic.

To compare the expressive power of $LTL_{lambda(=)}$ with propositional $LTL$, a bijection between (finitely many) non-temporal types in models of $LTL_{lambda(=)}$ and propositional variables is used.

References

[1] M. Fitting, Modal Logics Between Propositional and First-Order, Journal of Logic and Computation, 12, pp 1017-1026, 2002.

[2] A. Lisitsa and I. Potapov, Temporal logic with predicate abstraction, CoRR cs.LO/0410072, The Computing Research Repository, http://xxx.lanl.gov/archive/cs/, 14pp, 2004.

Mail to Webmaster alc9@math.nsc.ru

|Home Page| |English Part|

Go to Home