Abstract We present a technique for obtaining a logic with abductive reasoning extending a given propositional logic. Abduction, along with deduction and induction, is recognized as important for machine learning, namely in identifying possible causes that may lead to the occurrence of an event and in providing new ways for a computational device to achieve a certain objective. Each rule in the original calculus induces a set of multiple-conclusion abductive rules. Moreover, rules stating generic properties of abduction have to be added. In the induced logic, the deductive mechanism of the base logic coexists with this abductive component. A new notion of a multiple-conclusion derivation had to be developed. Due to the canonical nature of obtaining such a logic, we prove the preservation of soundness, completeness, decidability and computational complexity. These concepts and results are illustrated in a robot navigation problem using a multimodal logic.

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.

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.

Fibring is a metalogical constructor that permits to combine different logics by operating on their deductive systems under certain natural restrictions, as for example that the two given logics are presented by deductive systems of the same type. Under such circumstances, fibring will produce a new deductive system by means of the free use of inference rules from both deductive systems, provided the rules are schematic, in the sense of using variables that are open for application to formulas with new linguistic symbols (from the point of view of each logic component). Fibring is a generalization of fusion, a less general but wider developed mechanism which permits results of the following kind: if each logic component is decidable (or sound, or complete with respect to a certain semantics) then the resulting logic heirs such a property. The interest for such preservation results for combining logics is evident, and they have been achieved in the more general setting of fibring in several cases. The Craig interpolation property and the Maehara interpolation have a special significance when combining logics, being related to certain problems of complexity theory, some properties of model theory and to the usual (global) metatheorem of deduction. When the peculiarities of the distinction between local and global deduction interfere, justifying what we call careful reasoning, the question of preservation of interpolation becomes more subtle and other forms of interpolation can be distinguished. These questions are investigated and several (global and local) preservation results for interpolation are obtained for fibring logics that fulfill mild requirements.

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.

Abstract Fibring is recognized as one of the main mechanisms in combining logics, with great significance in the theory and applications of mathematical logic. However, an open challenge to fibring is posed by the collapsing problem: even when no symbols are shared, certain combinations of logics simply collapse to one of them, indicating that fibring imposes unwanted interconnections between the given logics. Modulated fibring allows a finer control of the combination, solving the collapsing problem both at the semantic and deductive levels. Main properties like soundness and completeness are shown to be preserved, comparison with fibring is discussed, and some important classes of examples are analyzed with respect to the collapsing problem.

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.