This paper investigates modular combinations of temporal logic systems. Four combination methods are described and studied with respect to the transfer of logical properties from the component one-dimensional temporal logics to the resulting combined two-dimensional temporal logic. Three basic logical properties are analyzed, namely soundness, completeness, and decidability. Each combination method comprises three submethods that combine the languages, the inference systems, and the semantics of two one-dimensional temporal logic systems, generating families of two-dimensional (...) temporal languages with varying expressivity and varying degrees of transfer of logical properties. The temporalization method and the independent combination method are shown to transfer all three basic logical properties. The method of full join of logic systems generates a considerably more expressive language but fails to transfer completeness and decidability in several cases. So a weaker method of restricted join is proposed and shown to transfer all three basic logical properties. (shrink)

In this paper we propose a very general de nition of combination of logics by means of the concept of sheaves of logics. We first discuss some properties of this general definition and list some problems, as well as connections to related work. As applications of our abstract setting, we show that the notion of possible-translations semantics, introduced in previous papers by the first author, can be described in categorial terms. Possible-translations semantics constitute illustrative cases, since they provide a new (...) semantical account for abstract logical systems, particularly for many-valued and paraconsistent logics. (shrink)

This paper generalises and complements the work on combining temporal logics started by Finger and Gabbay [11, 10]. We present proofs of transference of soundness, completeness and decidability for the temporalisation of logics T for any flow of time, eliminating the original restriction that required linear time for the transference of those properties through logic combination. We also generalise such results to the external application of a multi-modal system containing any number of connectives with arbitrary arity, that respect normality.This (...) generalisation over generic flows of time propagates to other combinations of logics that can be interpreted in terms of temporalisations. In this way, the independent combination of temporal logics is studied over generic flows of time. We show the transfer of soundness, completeness and decidability for independent combination of temporal logics. Finally, we also discuss the independent combination of any finite number of normal multi-modal logics. (shrink)

This paper shows Hilbert system (C+J)-, given by del Cerro and Herzig (1996) is semantically incomplete. This system is proposed as a proof theory for Kripke semantics for a combination of intuitionistic and classical propositional logic, which is obtained by adding the natural semantic clause of classical implication into intuitionistic Kripke semantics. Although Hilbert system (C+J)- contains intuitionistic modus ponens as a rule, it does not contain classical modus ponens. This paper gives an argument ensuring that the system (C+J)- (...) is semantically incomplete because of the absence of classical modus ponens. Our method is based on the logic of paradox, which is a paraconsistent logic proposed by Priest (1979). (shrink)

In recent years combinations of tense and modality have moved intothe focus of logical research. From a philosophical point of view, logical systems combining tense and modality are of interest because these logics have a wide field of application in original philosophical issues, for example in the theory of causation, of action, etc. But until now only methods yielding completeness results for propositional languages have been developed. In view of philosophical applications, analogous results with respect to languages of (...) predicate logic are desirable, and in this paper I present two such results. The main developments in this area can be split into two directions, differing in the question whether the ordering of time is world-independent or not. Semantically, this difference appears in the discussion whether T x W-frames or Kamp-frames (resp. Ockham-frames) provide a suitable semantics for combinations of tense and modality. Here, two calculi are presented, the first adequate with respect to Kamp-semantics, the second to T x Wsemantics. (Both calculi contain an appropriate version of Gabbay's irreflexivity rule.) Furthermore, the proposed constructions of canonical frames simplify some of those which have hitherto been discussed. (shrink)

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations (...) are not translated. Both translations are closely related in a canonical way. In a preceding paper, Barendregt, Bunder and Dekkers, 1993, we proved completeness of the two direct translations. In the present paper we prove completeness of the two indirect translations by showing that the corresponding illative systems are conservative over the two systems for the direct translations. In another version, DBB (1997), we shall give a more direct completeness proof. These papers fulfill the program of Church and Curry to base logic on a consistent system of $\lambda$ -terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). (shrink)

The work of the Brussels-Austin groups on irreversibility over the last years has shown that Quantum Large Poincaré systems with diagonal singularity lead to an extension of the conventional formulation of dynamics at the level of mixtures which is manifestly time asymmetric. States with diagonal singularity acquire meaning as linear fractionals over the involutive Banach algebra of operators with diagonal singularity. We show in this paper that the logic of quantum systems with diagonal singularity is not the (...) conventional logic of Hilbert space, because only finite combinations of prepositions are allowed. (shrink)

Although a very recent topic in contemporary logic, the subject of combinations of logics has already shown its deep possibilities. Besides the pure philosophical interest offered by the possibility of defining mixed logic systems in which distinct operators obey logics of different nature, there are also several pragmatical and methodological reasons for considering combined logics. We survey methods for combining logics (integration of several logic systems into a homogeneous environment) as well as methods for (...) decomposing logics, showing their interesting properties and applications. (shrink)

Fusion is a well-known form of combining normal modal logics endowed with a Hilbert calculi and a Kripke semantics. Herein, fusion is studied over logic systems using sequent calculi labelled with truth values and with a semantics based on a two-sorted algebra allowing, in particular, the representation of general Kripke structures. A wide variety of logics, including non-classical logics like, for instance, modal logics and intuitionistic logic can be presented by logic systems of this kind. (...) A categorical approach of fusion is defined in the context of these logic systems. Preservation of soundness and completeness by fusion is studied. Soundness is preserved without further requirements, completeness is preserved under mild assumptions. (shrink)

We draw parallels between several closely related logics that combine — in different proportions — elements of game theory, computation tree logics, and epistemic logics to reason about agents and their abilities. These are: the coalition game logics CL and ECL introduced by Pauly 2000, the alternating-time temporal logic ATL developed by Alur, Henzinger and Kupferman between 1997 and 2002, and the alternating-time temporal epistemic logic ATEL by van der Hoek and Wooldridge (2002). In particular, we establish some (...) subsumption and equivalence results for their semantics, as well as interpretation of the alternating-time temporal epistemic logic into ATL. The focus in this paper is on models: alternating transition systems, multi-player game models (alias concurrent game structures) and coalition effectivity models turn out to be intimately related, while alternating epistemic transition systems share much of their philosophical and formal apparatus. Our approach is constructive: we present ways to transform between different types of models and languages. (shrink)

We combine intuitionistic logic and classical logic into a new, first-order logic called polarized intuitionistic logic. This logic is based on a distinction between two dual polarities which we call red and green to distinguish them from other forms of polarization. The meaning of these polarities is defined model-theoretically by a Kripke-style semantics for the logic. Two proof systems are also formulated. The first system extends Gentzenʼs intuitionistic sequent calculus LJ. In addition, this (...) system also bears essential similarities to Girardʼs LC proof system for classical logic. The second proof system is based on a semantic tableau and extends Dragalinʼs multiple-conclusion version of intuitionistic sequent calculus. We show that soundness and completeness hold for these notions of semantics and proofs, from which it follows that cut is admissible in the proof systems and that the propositional fragment of the logic is decidable. (shrink)

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. (shrink)

Interval type-2 fuzzy logic systems have favorable abilities to cope with uncertainties in many applications. While the block type-reduction under the guidance of inference plays the central role in the systems, Karnik-Mendel iterative algorithms are standard algorithms to perform the type-reduction; however, the high computational cost of type-reduction process may hinder them from real applications. The comparison between the KM algorithms and other alternative algorithms is still an open problem. This paper introduces the related theory of interval (...) type-2 fuzzy sets and discusses the blocks of fuzzy reasoning, type-reduction, and defuzzification of interval type-2 fuzzy logic systems by combining the Nagar-Bardini and Nie-Tan noniterative algorithms for solving the centroids of output interval type-2 fuzzy sets. Moreover, the continuous version of NT algorithms is proved to be accurate algorithms for performing the type-reduction. Four computer simulation examples are provided to illustrate and analyze the performances of two kinds of noniterative algorithms. The NB and NT algorithms are superior to the KM algorithms on both calculation accuracy and time, which afford the potential application value for designer and adopters of type-2 fuzzy logic systems. (shrink)

This Handbook documents the main trends in current research between logic and language, including its broader influence in computer science, linguistic theory and cognitive science. The history of the combined study of Logic and Linguistics goes back a long way, at least to the work of the scholastic philosophers in the Middle Ages. At the beginning of this century, the subject was revitalized through the pioneering efforts of Gottlob Frege, Bertrand Russell, and Polish philosophical logicians such as Kazimierz (...) Ajdukiewicz. Around 1970, the landmark achievements of Richard Montague established a junction between state-of-the-art mathematical logic and generative linguistic theory. Over the subsequent decades, this enterprise of Montague Grammar has flourished and diversified into a number of research programs with empirical and theoretical substance. This appears to be the first Handbook to bring logic-language interface to the fore. Both aspects of the interaction between logic and language are demonstrated in the book i.e. firstly, how logical systems are designed and modified in response to linguistic needs and secondly, how mathematical theory arises in this process and how it affects subsequent linguistic theory. The Handbook presents concise, impartial accounts of the topics covered. Where possible, an author and a commentator have cooperated to ensure the proper breadth and technical content of the papers. The Handbook is self-contained, and individual articles are of the highest quality. (shrink)

Normative arrow update logic (NAUL) is a logic that combines normative temporal logic (NTL) and arrow update logic (AUL). In NAUL, norms are interpreted as arrow updates on labeled transition systems with a CTL-like logic. We show that the satisfiability problem of NAUL is decidable with a tableau method and it is in EXPSPACE.

Motivated by applications in software engineering, we propose two forms of combination of logics: synchronization on formulae and synchronization on models. We start by reviewing satisfaction systems, consequence systems, one-step derivation systems and theory spaces, as well as their functorial relationships. We define the synchronization on formulae of two consequence systems and provide a categorial characterization of the construction. For illustration we consider the synchronization of linear temporal logic and equational logic. We define the (...) synchronization on models of two satisfaction systems and provide a categorial characterization of the construction. We illustrate the technique in two cases: linear temporal logic versus equational logic; and linear temporal logic versus branching temporal logic. Finally, we lift the synchronization on formulae to the category of logics over consequences systems. (shrink)

The probabilization of a logic system consists of enriching the language (the formulas) and the semantics (the models) with probabilistic features. Such an operation is said to be exogenous if the enrichment is done on top, without internal changes to the structure, and is called endogenous otherwise. These two different enrichments can be applied simultaneously to the language and semantics of a same logic. We address the problem of studying the transference of metaproperties, such as completeness and decidability, (...) to the exogenous probabilization of an abstract logic system. First, we setup the necessary framework to handle the probabilization of a satisfaction system by proving transference results within a more general context. In this setup, we define a combination mechanism of logics through morphisms and prove sufficient condition to guarantee completeness and decidability. Then, we demonstrate that probabilization is a special case of this exogenous combination method, and that it fulfills the general conditions to obtain transference of completeness and decidability. Finally, we motivate the applicability of our technique by analyzing the probabilization of the linear temporal logic over Markov chains, which constitutes an endogenous probabilization. The results are obtained first by studying the exogenous semantics, and then by establishing an equivalence with the original probabilization given by Markov chains. (shrink)

In many logics dealing with information one needs to make statements not only about cognitive states, but also about transitions between them. In this paper we analyze a dynamic modal logic that has been designed with this purpose in mind. On top of an abstract information ordering on states it has instructions to move forward or backward along this ordering, to states where a certain assertion holds or fails, while it also allows combinations of such instructions by means (...) of operations from relation algebra. In addition, the logic has devices for expressing whether in a given state a certain instruction can be carried out, and whether that state can be arrived at by carrying out a certain instruction.This paper deals mainly with technical aspects of our dynamic modal logic. It gives an exact description of the expressive power of this language; it also contains results on decidability for the language with arbitrary structures and for the special case with a restricted class of admissible structures. In addition, a complete axiomatization is given. The paper concludes with a remark about the modal algebras appropriate for our dynamic modal logic, and some questions for further work. (shrink)

This book constitutes the refereed proceedings of the 4th International Conference on Frontiers of Combining Systems, FroCoS 2002, held in Santa Margherita Ligure, Italy, in April 2002.The 14 revised full papers presented together with 3 invited papers were carefully reviewed and selected from 35 submissions. Among the topics covered are combination of logics, combination of constraint solving techniques, combination of decision procedures, combination problems in verification, modular problems of theorem proving, and the integration of decision procedures and other solving (...) processes into constraint programming and deduction systems. (shrink)

On the example of the online game Akinator, the basic principles on which programs of this type are built are considered. Effective technics have been proposed by which artificial intelligence systems can build logical inferences that allow to identify an unknown subject from its description. To confirm the considered hypotheses, the terminological analysis of definition of the program "Akinator" offered by the author is carried out. Starting from the assumptions given by the author's definition, the article complements their definitions (...) presented by other researchers and analyzes their constituent theses. Finally, some proposals are made for the next steps in improving the program. The Akinator program, at one time, became one of the most famous online games using artificial intelligence. And although this was not directly stated, it was clear to the experts in the field of artificial intelligence that the program uses the techniques of expert systems and is built on inference rules. At the moment, expert systems have lost their positions in comparison with the direction of neural networks in the field of artificial intelligence, however, in the case considered in the article, we are talking about techniques using both directions – hybrid systems. Games for filling semantics interact with the user, expanding their semantic base and use certain strategies to achieve the best result. The playful form of such semantics filling programs is beneficial for researchers by involving a large number of players. The article examines the techniques used by the Akinator program, and also suggests possible modifications to it in the future. This study, first of all, focuses on how the knowledge base of the Akinator program is built, it consists of incomplete sets, which can be filled and adjusted as a result of further iterations of the program launches. It is important to note our assumption that the order of questions used by the program during the game plays a key role, because it determines its strategy. It was identified that the program is guided by the principles of nonmonotonic logic – the assumptions constructed by the program are not final and can be rejected by it during the game. The three main approaches to acquisite semantics proposed by Jakub Šimko and Mária Bieliková are considered, namely, expert work, crowdsourcing and machine learning. Paying attention to machine learning, the Akinator program using machine learning to build an effective strategy in the game presents a class of hybrid systems that combine the principles of two main areas in artificial intelligence programs – expert systems and neural networks. (shrink)

We introduce a methodology whereby an arbitrary logic system L can be enriched with temporal features to create a new system T(L). The new system is constructed by combining L with a pure propositional temporal logic T (such as linear temporal logic with “Since” and “Until”) in a special way. We refer to this method as “adding a temporal dimension to L” or just “temporalising L”. We show that the logic system T(L) preserves several properties of (...) the original temporal logic like soundness, completeness, decidability, conservativeness and separation over linear flows of time. We then focus on the temporalisation of first-order logic, and a comparison is make with other first-order approaches to the handling of time. (shrink)

We introduce a methodology whereby an arbitrary logic system L can be enriched with temporal features to create a new system T(L). The new system is constructed by combining L with a pure propositional temporal logic T (such as linear temporal logic with Since and Until) in a special way. We refer to this method as adding a temporal dimension to L or just temporalising L. We show that the logic system T(L) preserves several properties of (...) the original temporal logic like soundness, completeness, decidability, conservativeness and separation over linear flows of time. We then focus on the temporalisation of first-order logic, and a comparison is make with other first-order approaches to the handling of time. (shrink)

A graph-theoretic account of logics is explored based on the general notion of m-graph (that is, a graph where each edge can have a finite sequence of nodes as source). Signatures, interpretation structures and deduction systems are seen as 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 nondeterministic semantics, and subsume all logics endowed with an algebraic semantics. (shrink)

In many logics dealing with information one needs to make statements not only about cognitive states, but also about transitions between them. In this paper we analyze a dynamic modal logic that has been designed with this purpose in mind. On top of an abstract information ordering on states it has instructions to move forward or backward along this ordering, to states where a certain assertion holds or fails, while it also allows combinations of such instructions by means (...) of operations from relation algebra. In addition, the logic has devices for expressing whether in a given state a certain instruction can be carried out, and whether that state can be arrived at by carrying out a certain instruction. This paper deals mainly with technical aspects of our dynamic modal logic. It gives an exact description of the expressive power of this language; it also contains results on decidability for the language with 'arbitrary' structures and for the special case with a restricted class of admissible structures. In addition, a complete axiomatization is given. The paper concludes with a remark about the modal algebras appropriate for our dynamic modal logic, and some questions for further work. The paper only contains some sketchy examples showing how the logic can be used to capture situations of dynamic interest, far more detailed applications are given in a companion to this paper (De Rijke [33]). (shrink)

The construction of a systematic philosophical foundation for logic is a notoriously difficult problem. In Part One I suggest that the problem is in large part methodological, having to do with the common philosophical conception of “providing a foundation”. I offer an alternative to the common methodology which combines a strong foundational requirement with the use of non-traditional, holistic tools to achieve this result. In Part Two I delineate an outline of a foundation for logic, employing the new (...) methodology. The outline is based on an investigation of why logic requires a veridical justification, i.e., a justification which involves the world and not just the mind, and what features or aspect of the world logic is grounded in. Logic, the investigation suggests, is grounded in the formal aspect of reality, and the outline proposes an account of this aspect, the way it both constrains and enables logic, logic's role in our overall system of knowledge, the relation between logic and mathematics, the normativity of logic, the characteristic traits of logic, and error and revision in logic. (shrink)

We investigate the system TRC of untyped illative combinatory logic that is equiconsistent with New Foundations. We prove that various unstratified combinators do not exist in TRC.

Satisfaction systems and reductions between them are presented as an appropriate context for analyzing the satisfiability and the validity problems. The notion of reduction is generalized in order to cope with the meet-combination of logics. Reductions between satisfaction systems induce reductions between the respective satisfiability problems and (under mild conditions) also between their validity problems. Sufficient conditions are provided for relating satisfiability problems to validity problems. Reflection results for decidability in the presence of reductions are established. The validity (...) problem in the meet-combination is proved to be decidable whenever the validity problem for the components are decidable. Several examples are discussed, namely, involving modal and intuitionistic logics, as well as the meet-combination of modal logic and intuitionistic logic. (shrink)

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are (...) not translated. Both translations are closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the program of Church [1932], [1933] and Curry [1930] to base logic on a consistent system of λ-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). (shrink)

This article introduces, studies, and applies a new system of logic which is called ‘HYPE’. In HYPE, formulas are evaluated at states that may exhibit truth value gaps and truth value gluts. Simple and natural semantic rules for negation and the conditional operator are formulated based on an incompatibility relation and a partial fusion operation on states. The semantics is worked out in formal and philosophical detail, and a sound and complete axiomatization is provided both for the propositional and (...) the predicate logic of the system. The propositional logic of HYPE is shown to contain first-degree entailment, to have the Finite Model Property, to be decidable, to have the Disjunction Property, and to extend intuitionistic propositional logic conservatively when intuitionistic negation is defined appropriately by HYPE’s logical connectives. Furthermore, HYPE’s first-order logic is a conservative extension of intuitionistic logic with the Constant Domain Axiom, when intuitionistic negation is again defined appropriately. The system allows for simple model constructions and intuitive Euler-Venn-like diagrams, and its logical structure matches structures well-known from ordinary mathematics, such as from optimization theory, combinatorics, and graph theory. HYPE may also be used as a general logical framework in which different systems of logic can be studied, compared, and combined. In particular, HYPE is found to relate in interesting ways to classical logic and various systems of relevance and paraconsistent logic, many-valued logic, and truthmaker semantics. On the philosophical side, if used as a logic for theories of type-free truth, HYPE is shown to address semantic paradoxes such as the Liar Paradox by extending non-classical fixed-point interpretations of truth by a conditional as well-behaved as that of intuitionistic logic. Finally, HYPE may be used as a background system for modal operators that create hyperintensional contexts, though the details of this application need to be left to follow-up work. (shrink)

"Hegel's Philosophy of Nature was for a long time regarded as an outdated historical curiosity. Yet if systematic completeness is given up, the value of Hegelian arguments and of Hegelian logic generally becomes uncertain. In this book, John Burbidge reveals the abiding significance of the Philosophy of Nature as the intermediate movement in Hegel's system." "Burbidge looks at three specific texts in Hegel's work: the two chapters of the Science of Logic that deal with the concept of chemism, (...) and the section on chemical process in the Philosophy of Nature. Through his detailed commentary, he clarifies Hegel's distinction between a strictly theoretical philosophy and one that understands the natural world. He shows that Hegel does not presume to derive natural data a priori, nor is he simply dependent on the explanatory theories arrived at by chemists themselves. Experience provides the data, but thought sets the parameters. Burbidge sets Hegel's thought in context with sketches of what Kant, Fichte, and Schelling had to say about chemistry, and with background outlining the stage chemistry had reached at the time Hegel was writing. He also reveals how Hegel changed his mind as he revised each section for succeeding editions of his work, thus providing a fascinating case study of the development of Hegel's ideas."--BOOK JACKET.Title Summary field provided by Blackwell North America, Inc. All Rights Reserved. (shrink)

The International workshop 'Frontiers of Combining Systems' is the only forum that is exclusively devoted to research efforts in this interdisciplinary area. This volume contains selected, edited papers from the second installment of the workshop. The contributions range from theorem proving, rewriting and logic to systems and constraints. While there is a clear emphasis on automated tools and logics, the contributions to this volume show that there exists a rapidly expanding body of solutions of particular instances of (...) the combination problem, and at the same time, that the issue of developing general frameworks for intergrating formalisms and systems is taking on an increasingly important position on the international research agenda. The idea of combining formal systems and algorithms has been attracting interest in areas as diverse as constraint logic programming, automated deduction, verification, information retrieval, computational linguistics, artificial intelligence, and logic. As any interesting real world system is a complex composite entity, decomposing its descriptive requirements (for design, verification, or maintenance purposes) into simpler, more restricted tasks is appealing as it is often the only plausible way of tackling complex modelling problems. A core body of notions, questions and results is beginning to emerge in the area, and we are beginning to understand the computational and logical impact of combining methods and algorithms. (shrink)

We propose various methods for combining or amalgamating propositional languages and deductive systems. We make heavy use of quantales and quantale modules in the wake of previous works by the present and other authors. We also describe quite extensively the relationships among the algebraic and order-theoretic constructions and the corresponding ones based on a purely logical approach.

Combining logics has become a rapidly expanding enterprise that is inspired mainly by concerns about modularity and the wish to join together tailor made logical tools into more powerful but still manageable ones. A natural question is whether it offers anything new over and above existing standard languages. By analysing a number of applications where combined logics arise, we argue that combined logics are a potentially valuable tool in applied logic, and that endorsements of standard languages often miss the (...) point. Using the history of quantified modal logic as our main example, we also show that the use of combined structures and logics is a recurring theme in the analysis of existing logical systems. (shrink)

In many logics dealing with information one needs to make statements not only about cognitive states, but also about transitions between them. In this paper we analyze a dynamic modal logic that has been designed with this purpose in mind. On top of an abstract information ordering on states it has instructions to move forward or backward along this ordering, to states where a certain assertion holds or fails, while it also allows combinations of such instructions by means (...) of operations from relation algebra. In addition, the logic has devices for expressing whether in a given state a certain instruction can be carried out, and whether that state can be arrived at by carrying out a certain instruction. (shrink)

This is Part 1 of a paper on fibred semantics and combination of logics. It aims to present a methodology for combining arbitrary logical systems L i , i ∈ I, to form a new system L I . The methodology `fibres' the semantics K i of L i into a semantics for L I , and `weaves' the proof theory (axiomatics) of L i into a proof system of L I . There are various ways of doing this, (...) we distinguish by different names such as `fibring', `dovetailing' etc, yielding different systems, denoted by L F I , L D I etc. Once the logics are `weaved', further `interaction' axioms can be geometrically motivated and added, and then systematically studied. The methodology is general and is applied to modal and intuitionistic logics as well as to general algebraic logics. We obtain general results on bulk, in the sense that we develop standard combining techniques and refinements which can be applied to any family of initial logics to obtain further combined logics. The main results of this paper is a construction for combining arbitrary, (possibly not normal) modal or intermediate logics, each complete for a class of (not necessarily frame) Kripke models. We show transfer of recursive axiomatisability, decidability and finite model property. Some results on combining logics (normal modal extensions of K) have recently been introduced by Kracht and Wolter, Goranko and Passy and by Fine and Schurz as well as a multitude of special combined systems existing in the literature of the past 20-30 years. We hope our methodology will help organise the field systematically. (shrink)

This reply to Oaksford and Chater’s ’s critical discussion of our use of logic programming to model and predict patterns of conditional reasoning will frame the dispute in terms of the semantics of the conditional. We begin by outlining some common features of LP and probabilistic conditionals in knowledge-rich reasoning over long-term memory knowledge bases. For both, context determines causal strength; there are inferences from the absence of certain evidence; and both have analogues of the Ramsey test. Some current (...) work shows how a combination of counting defeaters and statistics from network monitoring can provide the information for graded responses from LP reasoning. With this much introduction, we then respond to O&C’s specific criticisms and misunderstandings. (shrink)

The Joint International Conference on Logic Programming, sponsored by the Association for Logic Programming, is a major forum for presentations of research, applications, and implementations in this important area of computer science. Logic programming is one of the most promising steps toward declarative programming and forms the theoretical basis of the programming language Prolog and its various extensions. Logic programming is also fundamental to work in artificial intelligence, where it has been used for nonmonotonic and commonsense (...) reasoning, expert systems implementation, deductive databases, and applications such as computer-aided manufacturing. Krzysztof R. Apt is project leader at the Centre for Mathematics and Computer Science in Amsterdam and part-time Professor in Computer Science at the University of Amsterdam. Topics covered: Theory Foundations. Programming Languages. Implementation. Programming Methodologies and Tools. Applications. Deductive Databases. Artificial Intelligence. Parallelism. (shrink)

Linear Logic is a versatile framework with diverse applications in computer science and mathematics. One intriguing fragment of Linear Logic is Multiplicative-Additive Linear Logic (MALL), which forms the exponential-free component of the larger framework. Modifying MALL, researchers have explored weaker logics such as Noncommutative MALL (Bilinear Logic, BL) and Cyclic MALL (CyMALL) to investigate variations in commutativity. In this paper, we focus on Cyclic Nonassociative Bilinear Logic (CyNBL), a variant that combines noncommutativity and nonassociativity. We (...) introduce a sequent system for CyNBL, which includes an auxiliary system for incorporating nonlogical axioms. Notably, we establish the cut elimination property for CyNBL. Moreover, we establish the strong conservativeness of CyNBL over Full Nonassociative Lambek Calculus (FNL) without additive constants. The paper highlights that all proofs are constructed using syntactic methods, ensuring their constructive nature. We provide insights into constructing cut-free proofs and establishing a logical relationship between CyNBL and FNL. (shrink)

This anthology contains revised versions of selected papers presented at the the fourth bi-annual international deontic logic conference, DEON’06. There is a substantial introduction (see separate entry), papers from all four invited speakers, David Makinson, Donald Nute, Claudio Pizzi, and Georg Von Wright. After the introduction and lead chapter "Deontic Logic - as I See It" by G.H. von Wright, there are nineteen articles grouped under six headings, "Norms and Truth", "Agency and Time", "Analysis of Normative Conflicts", "Defeasibility (...) and Norm Conflicts", Computer System Applications", and "Combinations of Logics". The collection contains a number of influential articles and a large array of key authors in deontic logic contribute. (shrink)

This paper studies a combined system of intuitionistic and classical propositional logic from proof-theoretic viewpoints. Based on the semantic treatment of Humberstone (J Philos Log 8:171–196, 1979) and del Cerro and Herzig (Frontiers of combining systems: FroCoS, Springer, 1996), a sequent calculus $$\textsf{G}(\textbf{C}+\textbf{J})$$ is proposed. An approximate idea of obtaining $$\textsf{G}(\textbf{C}+\textbf{J})$$ is adding rules for classical implication on top of the intuitionistic multi-succedent sequent calculus by Maehara (Nagoya Math J 7:45–64, 1954). However, in the semantic treatment, some formulas (...) do not satisfy heredity, which leads to the necessity of a restriction on the right rule for intuitionistic implication to keep the soundness of the calculus. The calculus $$\textsf{G}(\textbf{C}+\textbf{J})$$ enjoys cut elimination and Craig interpolation, whose detailed proofs are described in this paper. Cut elimination enables us to show the decidability of this combination both directly and syntactically. This paper also employs a canonical model argument to establish the strong completeness of Hilbert system $$\mathbf {C+J}$$ proposed by del Cerro and Herzig (Frontiers of combining systems: FroCoS, Springer, 1996). (shrink)

This is Part 1 of a paper on fibred semantics and combination of logics. It aims to present a methodology for combining arbitrary logical systems $\mathbf{L}_i, i \in I$, to form a new system $\mathbf{L}_I$. The methodology `fibres' the semantics $\mathscr{K}_i$ of $\mathbf{L}_i$ into a semantics for $\mathbf{L}_I$, and `weaves' the proof theory of $\mathbf{L}_i$ into a proof system of $\mathbf{L}_I$. There are various ways of doing this, we distinguish by different names such as `fibring', `dovetailing' etc, yielding different (...) systems, denoted by $\mathbf{L}^F_I, \mathbf{L}^D_I$ etc. Once the logics are `weaved', further `interaction' axioms can be geometrically motivated and added, and then systematically studied. The methodology is general and is applied to modal and intuitionistic logics as well as to general algebraic logics. We obtain general results on bulk, in the sense that we develop standard combining techniques and refinements which can be applied to any family of initial logics to obtain further combined logics. The main results of this paper is a construction for combining arbitrary, modal or intermediate logics, each complete for a class of Kripke models. We show transfer of recursive axiomatisability, decidability and finite model property. Some results on combining logics have recently been introduced by Kracht and Wolter, Goranko and Passy and by Fine and Schurz as well as a multitude of special combined systems existing in the literature of the past 20-30 years. We hope our methodology will help organise the field systematically. (shrink)

A conception of an information system has been introduced by Pawlak. The study has been continued in works of Pawlak and Orlowska and in works of Vakarelov. They had proposed some basic relations and had constructed a formal system of a modal logic that describes the relations and some of their Boolean combinations. Our work is devoted to a generalization of this approach. A class of relation systems and a complete calculus construction method for these systems (...) are proposed. As a corollary of our main result, our paper contains a solution of a Vakarelov's problem: how to construct a formal system that describes all the Boolean combinations of the basic relations. (shrink)

Rice Combinational and Sequential Logic This text provides a guide to combinational and sequential logic, introducing students to the basic concepts then progressing to HND/first year undergraduate level. It has a highly practical emphasis, enabling the reader to simulate, build and test the circuits discussed in the text. Electronics Workbench files are provided for simulation, while easy-to-use XPLA software and specially designed hardware encourage the reader to build and test the circuits using programmable logic. The text itself (...) contains many self-assessment questions, complete with detailed answers, allowing students to test themselves as they learn. No previous experience of the topic is required and an abundance of practical examples helps students to apply the basic principles. The accompanying CD-ROM provides the XPLA development system software and Electronics Workbench files, as well as the Xilinx Webpack development system and 'walkthrough'. Hardware for Programmable Logic experiments can either be purchased or built following instructions from the text. Altogether, the text, software and hardware provide an interactive and stimulating teaching and learning resource. F. (shrink)

This book addresses the hasty development of modern logic, especially its introducing and embracing various kinds of artificial languages and moving from the study of natural languages to that of artificial ones. This shift seemed extremely helpful and managed to elevate logic to a new level of rigor and clarity. However, the change that logic underwent in this way was in no way insignificant, and it is also far from an insignificant matter to determine to what extent (...) the "new logic" only engaged new and more powerful instruments to answer the questions posed by the "old" one, and to what extent it replaced these questions with new ones. Hence, this movement has generated brand new kinds of philosophical problems that have still not been dealt with systematically. Philosophy of Logical Systems addresses these new kinds of philosophical problems that are intertwined with the development of modern logic. Jaroslav Peregrin analyzes the rationale behind the introduction of the artificial languages of logic; classifies the various tools which were adopted to build such languages; gives an overview of the various kinds of languages introduced in the course of modern logic and the motifs of their employment; discusses what can actually be achieved by relocating the problems of logic from natural language into them; and reaches certain conclusions with respect to the possibilities and limitations of this "formal turn" of logic. This book is both an important scholarly contribution to the philosophy of logic and a systematic survey of the standard logical systems that were established during the short history of modern logic. (shrink)

We study probabilistic logic under the viewpoint of the coherence principle of de Finetti. In detail, we explore how probabilistic reasoning under coherence is related to model- theoretic probabilistic reasoning and to default reasoning in System . In particular, we show that the notions of g-coherence and of g-coherent entailment can be expressed by combining notions in model-theoretic probabilistic logic with concepts from default reasoning. Moreover, we show that probabilistic reasoning under coherence is a generalization of default reasoning (...) in System . That is, we provide a new probabilistic semantics for System , which neither uses infinitesimal probabilities nor atomic bound (or big-stepped) probabilities. These results also provide new algorithms for probabilistic reasoning under coherence and for default reasoning in System , and they give new insight into default reasoning with conditional objects. (shrink)

Combinatory logic is known to be related to substructural logics. Algebraic considerations of the latter, in particular, algebraic considerations of two distinct implications, led to the introduction of dual combinators in Dunn & Meyer 1997. Dual combinators are "mirror images" of the usual combinators and as such do not constitute an interesting subject of investigation by themselves. However, when combined with the usual combinators, the whole system exhibits new features. A dual combinatory system with weak equality typically lacks the (...) Church-Rosser property, and in general it is inconsistent. In many subsystems terms "unexpectedly" turn out to be weakly equivalent. The paper is a preliminary attempt to investigate some of these issues, as well as, briefly compare function application in symmetric -calculus and dual combinatory logic. (shrink)