A simple notion of quantum Turing machine with deterministic, classical control is proposed and shown to be powerful enough to compute any unitary transformation that is computable by a finitely generated quantum circuit. An efficient universal machine with the s-m-n property is presented. The BQP class is recovered. A robust notion of plain Kolmogorov complexity of quantum states is proposed and compared with those previously reported in the literature.

A complete extension of classical propositional logic is proposed for reasoning about circuits with unreliable gates. The pitfalls of extrapolating classical reasoning to such unreliable circuits are extensively illustrated. Several metatheorems are shown to hold with additional provisos. Applications are provided in verification of logic circuits and improving their reliability.

When combining logics while imposing the sharing of connectives, the result is frequently inconsistent. In fact, in fibring, fusion and other forms of combination reported in the literature, each shared connective inherits the logical properties of each of its components. A new form of combining logics (meet-combination) is proposed where such a connective inherits only the common logical properties of its components. The conservative nature of the proposed combination is shown to hold without provisos. Preservation of soundness and completeness is also proved. Illustrations are provided involving classical, intuitionistic and modal logics.

Capitalising on the graph-theoretic account of fibring proposed in [31], we show that fibring preserves the finite model property under mild conditions. Illustrations are provided for modal, deontic, paraconsistent and linear logics.

A graph-theoretic account of logics is explored based on the general notion of m-graph (i.e; a graph where each edge can have a finite sequence of nodes as source). Signatures, interpretation structures and deduction systems are seen as multi-graphs (m-graphs). After defining a category freely generated by a m-graph, formulas and expressions in general can be seen as morphisms. Moreover, derivations involving rule instantiation are also morphisms. Soundness and completeness theorems are proved. As a consequence of the generality of the approach our results apply to very different logics encompassing, among others, substructural logics as well as logics with non-deterministic semantics, and subsume all logics endowed with an algebraic semantics.

A graph-theoretic account of fibring of logics is developed, capitalizing on the interleaving characteristics of fibring at the linguistic, semantic and proof levels. Fibring of two signatures is seen as a multi-graph (m-graph) where the nodes and the m-edges include the sorts and the constructors of the signatures at hand. Fibring of two models is a multi-graph (m-graph) where the nodes and the m-edges are the values and the operations in the models, respectively. Fibring of two deductive systems is an m-graph whose nodes are language expressions and the m-edges represent the inference rules of the two original systems. The sobriety of the approach is confirmed by proving that all the fibring notions are universal constructions. This graph-theoretic view is general enough to accommodate very different fibrings of propositional based logics encompassing logics with non-deterministic semantics, logics with an algebraic semantics, logics with partial semantics and substructural logics, among others. Soundness and weak completeness are proved to be preserved under very general conditions. Strong completeness is also shown to be preserved under tighter conditions. In this setting, the collapsing problem appearing in several combinations of logic systems can be avoided.

Following recent developments in the topic of generalized quantifiers, and also having in mind applications in the areas of security and artificial intelligence, a conservative enrichment of (two-sorted) first-order logic (FOL) with almost-everywhere quantification is proposed. The completeness of the axiomatization against the measure-heoretic semantics is carried out using a variant of the Lindenbaum–Henkin technique. The independence of the axioms is analysed, and the almost-everywhere quantifier is compared with related notions of generalized quantification. A suitable fragment of the logic is translated to FOL and validity is shown to be preserved.

The concept of fibring is extended to higher-order logics with arbitrary modalities and binding operators. A general completeness theorem is established for such logics including HOL and with the meta-theorem of deduction. As a corollary, completeness is shown to be preserved when fibring such rich logics. This result is extended to weaker logics in the cases where fibring preserves conservativeness of HOL-enrichments. Soundness is shown to be preserved by fibring without any further assumptions.

We give a categorial characterization of how labelled deduction systems for logics with a propositional basis behave under unconstrained fibring and under fibring that is constrained by symbol sharing. At the semantic level, we introduce a general semantics for our systems and then give a categorial characterization of fibring of models. Based on this, we establish the conditions under which our systems are sound and complete with respect to the general semantics for the corresponding logics, and establish requirements on logics and systems so that completeness is preserved by both forms of fibring.

Abstract A completeness theorem is established for logics with congruence endowed with general semantics (in the style of general frames). As a corollary, completeness is shown to be preserved by fibring logics with congruence provided that congruence is retained in the resulting logic. The class of logics with equivalence is shown to be closed under fibring and to be included in the class of logics with congruence. Thus, completeness is shown to be preserved by fibring logics with equivalence and general semantics. An example is provided showing that completeness is not always preserved by fibring ligics endowed with standard (non general) semantics. A categorial characterization of fibring is provided using coproducts and cocartesian liftings.

The purpose of this article is to extend the situation calculus, a logical framework for the specification of theories of action and change, with actions that have a non-deterministic or uncertain nature. Our approach is based upon the idea that actions may have a deterministic component, and a probabilistic component. For example, the act of flipping a coin has a deterministic component (the actual coin toss) and an uncertain component (the outcome). We extend the language of the situation calculus in order to make explicit this distinction between these two action components. Furthermore, we provide means to reason about the outcomes of processes specified only in terms of deterministic action components (which we call behaviors). In particular, we show how one can compute the probability that some fluent will hold after specific behavior is realized. An important feature of our approach is that the syntactic and semantic structure of actions and situations is independent of the decomposition of actions into deterministic and uncertain components. Thus, we inherit solutions to the frame problem ramification problem, etc.

Much attention has been given recently to the mechanism of fibring of logics, allowing free mixing of the connectives and using proof rules from both logics. Fibring seems to be a rather useful and general form of combination of logics that deserves detailed study. It is now well understood at the proof-theoretic level. However, the semantics of fibring is still insufficiently understood. Herein we provide a categorial definition of both proof-theoretic and model-theoretic fibring for logics without terms. To this end, we introduce the categories of Hilbert calculi, interpretation systems and logic system presentations. By choosing appropriate notions of morphism it is possible to obtain pure fibring as a coproduct. Fibring with shared symbols is then easily obtained by coCarteisan lifting from the category of signatures. Soundness is shown to be preserved by these constructions. We illustrate the constructions within prepositional modal logic. Key words: Logic morphism, combination of logics, fibring, fibred semantics, preservation of soundness, modal logic.

Abstract A denotational semantics and a sound and complete inequational proof systems for processes with varying degrees of liveness is presented. New insights on quiescence are given concerning the Jonsson characterisation of input/output system. A theory of transational behaviour of the type carry out until the end is developed as an application of this concept of process with liveness requirements. The proposed model fully reflects the parallel composition of transactional requirements , giving the expected composite requirements.

A logic for specifying and reasoning about object classes and their instances (aspects) is presented and illustrated. This logic is an extension of a rather standard linear temporal, many-sorted, first-order predicate logic with equality. The extensions were designed to be as simple as possible while supporting the envisaged locality of arguments, object specialization and object aggregation. Objects are specified through their aspects. Each aspect establishes a local vocabulary (signature). The logic works at two levels: first, we can specify and prove assertions about a given object aspect in isolation (local reasoning), e.g. persons, patients or cars; second, we can specify interaction constraints and make inferences between aspects within the same community of objects (global reasoning), e.g. carry the theorems of persons onto patients (specialization inheritance) or carry the theorems of persons onto the aggregations of persons and cars (incorporation inheritance). Some reflection mechanisms are also shown to be sound: for instance what becomes true of persons because of the interactions between persons and cars. The proposed logic is given in an axiomatic style.

An object is understood as adynamic entity whose attributes can be observed and modified through the occurences of its events. In order to reason about such an object, a logical language and a tableau method are presented in this paper. Objects and their properties and can be described by a set of formulate based on their signatures. The tableau method is an extension and a development of a first-order tableau method. To confute a finite set of formulae based on their signatures. The confute a finite set of formuale is to construct a set of tableaux and define some dependency relations on them. A simple illustrative example is also given to show how to reason about objects using our method.

Abstract A brief overview is given of the temporal logics used in concurrent program verification and in database and systems specification. The properties of the underlying modal frame structures are analysed. The relative advantages of the linear and branching approaches are discussed. The state versus path formulas controversy is revisited. A meta-linear operatorLis proposed and compared with the “in all trajectories” operator considered in the language CTL*. The usefulness of the new operator within the context of a layered methodology for database and information systems specification and verification is illustrated. The operator is seen as a “frame change operator” and other interesting operators of this class are referred. Finitary and infinitary axiomatisations are given for the operatorL. The proof of the completeness of the infinitary axiomatisation is briefly outlined. This proof requires an appropriate extension of the usual Henkin methods.

The use of modal qualification on terms is advocated for a more intuitive account of the description of the effects of events on objects such as program variables or database attributes, and also for an easier verification of the intended temporal integrity constraints. We develop two logics of modal terms focusing on positional and temporal qualification, and show by means of an example how they can be used to support the description and prescription of actions, as well as to reason about the properties of the specified systems.

SYSTEMATICS (a very high level specification language) is shown to be incomplete as a data base query language. Some extensions are proposed in order to ensure the desired degree of relational completeness. Moreover, the set-oriented SYSTEMATICS is compared with a predicate-oriented query language in order to assess the practical interest of the main construct of SYSTEMATICS (the identification construct). A proof of the completeness of the extended version of SYSTEMATICS is outlined. A concrete syntax for this version is proposed. The semantics of this extended version is developed within a set theoretic framework.