Labeled transition systems are key structures for modeling computation. In this paper, we show how they lend themselves to ordinary logical analysis (without any special new formalisms), by introducing their standard first-order theory. This perspective enables us to raise several basic model-theoretic questions of definability, axiomatization and preservation for various notions of process equivalence found in the computational literature, and answer them using well-known logical techniques (including the Compactness theorem, Saturation and Ehrenfeucht games). Moreover, we consider what happens to this (...) general theory when one restricts attention to special classes of transition systems (in particular, finite ones), as well as extended logical languages (in particular, infinitary first-order logic). We hope that this puts standard logical formalisms on the map as a serious option for a theory of computational processes. As a side benefit, our approach increases comparability with several other existing formalisms over labeled transition systems (such as Process Algebra or Modal Logic). We provide some pointers to this effect, too. (shrink)

Labeled transition systems are key structures for modeling computation. In this paper, we show how they lend themselves to ordinary logical analysis (without any special new formalisms), by introducing their standard first-order theory. This perspective enables us to raise several basic model-theoretic questions of definability, axiomatization and preservation for various notions of process equivalence found in the computational literature, and answer them using well-known logical techniques (including the Compactness theorem, Saturation and Ehrenfeucht games). Moreover, we consider what happens to this (...) general theory when one restricts attention to special classes of transition systems (in particular, finite ones), as well as extended logical languages (in particular, infinitary first-order logic). We hope that this puts standard logical formalisms on the map as a serious option for a theory of computational processes. As a side benefit, our approach increases comparability with several other existing formalisms over labeled transition systems (such as Process Algebra or Modal Logic). We provide some pointers to this effect, too. (shrink)

We propose a combination of Bochvar's strict three-valued logic, McCarthy's sequential three-valued logic, and process algebra via the conditional guard construct. This combination entails the introduction of a new constant meaningless in process algebra. We present an operational semantics in SOS-style, and a completeness result for ACP with conditional guard construct and the proposed logic.

A λ-theory T is a consistent set of equations between λ-terms closed under derivability. The degree of T is the degree of the set of Godel numbers of its elements. H is the $\lamda$ -theory axiomatized by the set {M = N ∣ M, N unsolvable. A $\lamda$ -theory is sensible $\operatorname{iff} T \supset \mathscr{H}$ , for a motivation see [6] and [4]. In § it is proved that the theory H is ∑ 0 2 -complete. We present Wadsworth's proof (...) that its unique maximal consistent extention $\mathscr{H}^\ast (= \mathrm{T}(D_\infty))$ is Π 0 2 -complete. In $\S2$ it is proved that $\mathscr{H}_\eta(= \lambda_\eta-\text{Calculus} + \mathscr{H})$ is not closed under the ω-rule (see [1]). In $\S3$ arguments are given to conjecture that $\mathscr{H}\omega (= \lambda + \mathscr{H} + omega-rule)$ is Π 1 1 -complete. This is done by representing recursive sets of sequence numbers as λ-terms and by connecting wellfoundedness of trees with provability in Hω. In $\S4$ an infinite set of equations independent over H η will be constructed. From this it follows that there are 2^{ℵ_0 sensible theories T such that $\mathscr{H} \subset T \subset \mathscr{H}^\ast$ and 2 ℵ 0 sensible hard models of arbitrarily high degrees. In $\S5$ some nonprovability results needed in $\S\S1$ and 2 are established. For this purpose one uses the theory H η extended with a reduction relation for which the Church-Rosser theorem holds. The concept of Gross reduction is used in order to show that certain terms have no common reduct. (shrink)

We apply a paraconsistent strategy to reasoning about fractions.

Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first is insufficient to determine the value of the expression. Com...

ABSTRACT We propose a combination of a fragment of four-valued logic and process algebra. This fragment is geared to a simple relation with process algebra via the conditional guard construct, and can easily be extended to a truth-functionally complete logic. We present an operational semantics in SOS-style, and a completeness result for ACP with conditionals and four- valued logic. Completeness is preserved under the restriction to some other non-classical logics.

We define and study the class of all stack algebras as the class of all minimal algebras in a variety defined by an infinite recursively enumerable set of equations. Among a number of results, we show that the initial model of the variety is computable, that its equational theory is decidable, but that its equational deduction problem is undecidable. We show that it cannot be finitely axiomatised by equations, but it can be finitely axiomatised by equations with a hidden sort (...) and functions. This class of all stack algebras, together with its specifications, can be used to survey the many models in the literature on stacks in a systematic way, and hence give the study of the stack some mathematical coherence. Article Outline. (shrink)