We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to the actions used in dynamic logics in order to define necessity and possibility operators. This leads to a higher degree of expressivity than that of many-sorted first-order logic. For example, one can finitely axiomatize both the finiteness and the reachability of models, neither of which are ordinarily possible in many-sorted first-order logic. We introduce syntactic entailment and study basic properties such as compactness and completeness, showing that the latter does not hold when standard finitary proof rules are used. Consequently, we define proof rules having both finite and countably infinite premises, and we provide conditions under which completeness can be proved. To that end, we generalize the forcing method introduced in model theory by Robinson from a single signature to a category of signatures, and we apply it to obtain a completeness result for signatures that are at most countable.

Transition systems provide a natural way to specify and reason about the behaviour of discrete systems, and in particular about the computations that they may perform. This paper advances a verification method for transition systems whose reachable states are described explicitly by membership axioms. The proof technique is implemented in the Constructor-based Inductive Theorem Prover (CITP), a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features. This approach complements the so-called OTS method, a verification procedure for observational transition systems that is already implemented in CITP.

We propose a logic-independent approach to logic programming through which the paradigm as we know it for Horn-clause logic can be explored for other formalisms. Our investigation is based on abstractions of notions such as logic program, clause, query, solution and computed answer, which we develop over Goguen and Burstall's theory of institutions. These give rise to a series of concepts that formalize the interplay between the denotational and the operational semantics of logic programming. We examine properties concerning the satisfaction of quantified sentences, discuss a variant of Herbrand's theorem that is not limited in scope to any particular logical system or construction of logic programs, and describe a general resolution-based procedure for computing solutions to queries. We prove that this procedure is sound; moreover, under additional hypotheses that reflect faithfully properties of actual logic-programming languages, we show that it is also complete.

More than a decade has passed since Herbrand’s theorem was first generalized to arbitrary institutions, enabling in this way the development of the logic-programming paradigm over formalisms beyond the conventional framework of relational first-order logic. Despite the mild assumptions of the original theory, recent developments have shown that the institution-based approach cannot capture constructions that arise when service-oriented computing is presented as a form of logic programming, thus prompting the need for a new perspective on Herbrand’s theorem founded instead upon a concept of generalized substitution system. In this paper, we formalize the connection between the institution- and the substitution-system-based approach to logic programming by investigating a number of features of institutions, like the existence of a quantification space or of representable substitutions, under which they give rise to suitable generalized substitution systems. Building on these results, we further show how the original institution independent versions of Herbrand’s theorem can be obtained as concrete instances of a more general result.