In this paper we prove that the reachability problem is BSS-undecidable for o-minimal dynamical systems.

Many industrial processes are operated in multiple modes due to different manufacturing strategies. Multimodality of process data is often accompanied with nonlinear and non-Gaussian characteristics, which makes data-driven monitoring more complicated. In this paper, statistics pattern analysis is introduced to extract low- and high-order statistics from raw process data. Support vector data description, which can deal with nonlinear and non-Gaussian problems, is applied to monitor multimode process in this paper. To improve detection performance of SVDD for training multimode data with (...) outliers, modified local reachability density ratio is proposed as a weight factor to be embedded in the weighted-SVDD model, in which the local neighbors in terms of both space and time are considered. Finally, the effectiveness and superiority of our proposed method are demonstrated by the Tennessee-Eastman process and wastewater treatment process. (shrink)

Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we propose a library for benchmarking Girard's (propositional) intuitionistic linear logic. For a quick bootstrapping of the collection of problems, and for discussing the selection of relevant problems and understanding their meaning as linear logic theorems, we use translations of the collection of Kleene's intuitionistic theorems in (...) the traditional monograph "Introduction to Metamathematics". We analyze four different translations of intuitionistic logic into linear logic and compare their proofs using a linear logic based prover with focusing. In order to enhance the set of problems in our library, we apply the three provability-preserving translations to the propositional benchmarks in the ILTP Library. Finally, we generate a comprehensive set of reachability problems for Petri nets and encode such problems as linear logic sequents, thus enlarging our collection of problems. (shrink)

We show that—unlike products of ‘transitive’ modal logics which are usually undecidable—their ‘expanding domain’ relativisations can be decidable, though not in primitive recursive time. In particular, we prove the decidability and the finite expanding product model property of bimodal logics interpreted in two-dimensional structures where one component—call it the ‘flow of time’—is • a finite linear order or a finite transitive tree and the other is composed of structures like • transitive trees/partial orders/quasi-orders/linear orders or only finite such structures expanding (...) over time. The decidability proof is based on Kruskal’s tree theorem, and the proof of non-primitive recursiveness is by reduction of the reachability problem for lossy channel systems. The result is used to show that the dynamic topological logic interpreted in topological spaces with continuous functions is decidable if the number of function iterations is assumed to be finite. (shrink)

The question at issue is to develop a computational interpretation of Linear Logic [8] and to establish exactly its expressive power. We follow the bottom-up approach. This involves starting with the simplest of the systems we are interested in, and then expanding them step-by-step. We begin with the !-Horn fragment of Linear Logic, which uses only positive literals, the linear implication ⊸, the tensor product ⊗, and the modal storage operator !. We give a complete computational interpretation for the !-Horn (...) fragment of Linear Logic and for some natural generalizations of it formed by introducing additive connectives. Here we use the well-known ‘ or ’-like connective ⊕, and, for the sake of the computational duality, we introduce a new ‘ and ’-like connective @ For !-Horn sequents, we prove that their derivability problem is directly equivalent to the reachability problem for Petri nets, which is known to be decidable [19]. For the -Horn fragment of Linear Logic, which uses only positive literals, the linear implication ⊸, the tensor product ⊗, the modal storage operator!, and the additive ‘disjunction’ ⊕, we prove that standard Minsky machines [21] can be directly encoded in this -Horn fragment. Standard Minsky machines can be directly encoded in the corresponding ‘dual’ -Horn fragment of Linear Logic, as well. As a corollary, both these fragments of Linear Logic are proved to be undecidable. (shrink)

This paper studies the expressive power that an extra first order quantifier adds to a fragment of monadic second order logic, extending the toolkit of Janin and Marcinkowski [JM01].We introduce an operation existsn on properties S that says "there are n components having S". We use this operation to show that under natural strictness conditions, adding a first order quantifier word u to the beginning of a prefix class V increases the expressive power monotonically in u. As a corollary, if (...) the first order quantifiers are not already absorbed in V, then both the quantifier alternation hierarchy and the existential quantifier hierarchy in the positive first order closure of V are strict.We generalize and simplify methods from Marcinkowski [Mar99] to uncover limitations of the expressive power of an additional first order quantifier, and show that for a wide class of properties S, S cannot belong to the positive first order closure of a monadic prefix class W unless it already belongs to W.We introduce another operation alt on properties which has the same relationship with the Circuit Value Problem as reach has with the Directed Reachability Problem. We use alt to show that Πn⊈ FO, Σn⊈ FO, and Δn+1⊈ FOB, solving some open problems raised in [Mat98]. (shrink)

There is a serious problem with arguing that God intended to lock the epistemology of the 7th century into the immutable text of the Qur’an, and then intended to hold Muslims hostage to this epistemological framework for all ages to come. Among other things, this would limit the dynamism and effectiveness of Divine text because the Qur’an would be for ever locked within a knowledge paradigm that is very difficult to retrieve or re-create. The author argues for the recognition (...) of three critical categories in Islamic theology: haqq, hikma and ma‘arifa. While haqq connotes the objective and constant truth, it is not reachable without hikma. Hikma is the balance [mizan] of truths in every historical moment with all of its contingencies. Ma‘arifa is the epistemology or the way to searching the objective and constant truth as well as the search for the hikma appropriate for each stage in human consciousness. The author contends that it is contrary to the very nature of a merciful and compassionate God to leave Muslims with a Revelation that is not fully equipped to deal with the altered states of consciousness and perceptions that are inevitable in every stage of human development. (shrink)

One might think that money pumps directed at agents with cyclic preferences can be avoided by foresight. This view was challenged two decades ago by the discovery of a money pump with foresight, which works against agents who use backward induction. But backward induction implausibly assumes that the agent would act rationally and retain her trust in her future rationality even at choice nodes that could only be reached if she were to act irrationally. This worry does not apply to (...) BI-terminating decision problems, where at each choice node backward induction prescribes a move that terminates further action. For BI-terminating decision problems, it is enough to assume that rationality and trust in rationality are retained at choice nodes reachable by rational moves. The old money pump with foresight was not BI-terminating. In this paper, we present a new money pump with foresight, one that is both BI-terminating and considerably simpler. (shrink)

In this article I consider the case of the surgical separation of conjoined twins resulting in the immediate and predictable death of the weaker one. The case was submitted to English law by the hospital, and the operation permitted against the parents’ wishes. I consider the relationship between the legal decision and the moral reasons adduced in its support, reasons gaining their force against the framework of much mainstream normative ethical theory. I argue that in a few morally dilemmatic situations, (...) such a legalistic–theoretical approach cannot plausibly accommodate certain irreducible and ineliminable features of the ethical experience of any concrete individual implicated in the situation, and that this failure partly undermines its self–appointed role of guiding such an individual's conduct. For example, the problem as experienced by the judge and by the parents might not be the same problem at all, and some of their respective reasons may be mutually unintelligible or impotent. I certainly do not argue for a rejection of law or of moral theory; I merely challenge their implicit claim to comprehensiveness and their fixation with an idealised and putatively universal rationality modelled on converging scientific enquiry. Finally, I claim that at least in the twins’ case there may be insufficient normative robustness to the conclusions reached, or indeed reachable, by the court in a situation where intuitions and moral reasons pull in fundamentally incommensurable directions; as such, there may be room for an acknowledgement of the spiritual, through a humble abstention from making a decision – which is not to be confused with deciding to do nothing. (shrink)

We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute, inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input in order to establish or refute the satisfaction relation between a given world and a formula. We (...) present a framework for local model checking of Hybrid Logic based on games. We show that these games are simple reachability games for ordinary Hybrid Logic and weak Büchi games for Hybrid Logic with operators interpreted over the transitive closure of the accessibility relation of the underlying Kripke frame, and show how to solve these games thus solving the local model checking problem. Since the first-order part of Hybrid Logic is inherently hard to localise in model checking, we give examples, in the end, of how global model checkers can be optimised in certain special cases using well-established techniques like fixpoint approximations and divide-and-conquer algorithms. (shrink)

The paper presents a novel method for the verification of security protocols’ time properties. The new method uses a translation to satisfiability modulo theories problem. In our approach, we model protocol users’ behaviours using networks of synchronized timed automata. Suitably specified correctness properties are defined as a reachability property of some chosen states in an automata network. Then, the network of timed automata and the property are translated to an SMT problem and checked using an SMT-solver and (...) a BMC algorithm. We consider the most important time properties of protocol executions using specially constructed time conditions. The new method was also implemented and experimentally evaluated for six well-known SPs. We also compared our new SMT-based technique with the corresponding SAT-based approach. (shrink)

We define a tableau calculus for the logic of only knowing and knowing at most ON, which is an extension of Levesque's logic of only knowing O. The method is based on the possible-world semantics of the logic ON, and can be considered as an extension of known tableau calculi for modal logic K45. From the technical viewpoint, the main features of such an extension are the explicit representation of "unreachable" worlds in the tableau, and an additional branch closure condition (...) implementing the property that each world must be either reachable or unreachable. The calculus allows for establishing the computational complexity of reasoning about only knowing and knowing at most. Moreover, we prove that the method matches the worst-case complexity lower bound of the satisfiability problem for both ON and O. With respect to [22], in which the tableau calculus was originally presented, in this paper we both provide a formal proof of soundness and completeness of the calculus, and prove the complexity results for the logic ON. (shrink)

Although it is known that reachability in undirected finite graphs can be expressed by an existential monadic second-order sentence, our main result is that this is not the case for directed finite graphs (even in the presence of certain "built-in" relations, such as the successor relation). The proof makes use of Ehrenfeucht-Fraisse games, along with probabilistic arguments. However, we show that for directed finite graphs with degree at most k, reachability is expressible by an existential monadic second-order sentence.

Whether or not quantum physics can account for molecular structure is a matter of considerable controversy. Three of the problems raised in this regard are the problems of molecular structure. We argue that these problems are just special cases of the measurement problem of quantum mechanics: insofar as the measurement problem is solved, the problems of molecular structure are resolved as well. In addition, we explore one consequence of our argument: that claims about the reduction or emergence of (...) molecular structure cannot be settled independently of the choice of a particular resolution to the measurement problem. Specifically, we consider how three standard putative solutions to the measurement problem inform our under- standing of a molecule in isolation, as well as of chemistry’s relation to quantum physics. (shrink)

Bertrand Russell was one of the greatest logicians since Aristotle, and one of the most important philosophers of the past two hundred years. As we approach the 125th anniversary of the Nobel laureate's birth, his works continue to spark debate, resounding with unmatched timeliness and power. The Problems of Philosophy, one of the most popular works in Russell's prolific collection of writings, has become core reading in philosophy. Clear and accessible, this little book is an intelligible and stimulating guide to (...) those problems of philosophy which often mistakenly lead to its status as too lofty and abstruse for the lay mind. Focusing on problems he believes will provoke positive and constructive discussion, Russell concentrates on knowledge rather than metaphysics, steering the reader through his famous 1910 distinction between "knowledge by acquaintance and knowledge by description," and introducing important theories of Descartes, Kant, Hegel, Hume, Locke, Plato, and others to lay the foundation for philosophical inquiry by general readers and scholars alike.With a new introduction by John Perry, this valuable work is a perfect introduction to the field and will continue to stimulate philosophical discussion as it has done for nearly forty years. (shrink)

These seventeen lectures given in 1963 focus largely on Kant, 'a thinker in whose work the question of morality is most sharply contrasted with other spheres of existence'. After discussing a number of the Kantian categories of moral philosophy, Adorno considers other, seemingly more immediate general problems, such as the nature of moral norms, the good life, and the relation of relativism and nihilism. In the course of the lectures, Adorno addresses a wide range of topics, including: theory and practice, (...) ethics as bad conscience, the repressive character, the problem of freedom, dialectics in Kant and Hegel, the nature of reason, the moral law as a given, psychoanalysis, the element of the Absurd, freedom and law, the Protestant tradition of morality, Hamlet, self-determination, phenomenology, the concept of the will, the idea of humanity, The Wild Duck, and Nietzsche's critique of morality. (shrink)

From interpreting the world to changing it, this book is a synthesis of Chomsky's early work on philosophy, linguistics, and politics.

The Problems of Philosophy is a 1912 book by Bertrand Russell, in which Russell attempts to create a brief and accessible guide to the problems of philosophy. Focusing on problems he believes will provoke positive and constructive discussion, Russell concentrates on knowledge rather than metaphysics: If it is uncertain that external objects exist, how can we then have knowledge of them but by probability. There is no reason to doubt the existence of external objects simply because of sense data. Russell (...) guides the reader through his famous 1910 distinction between knowledge by acquaintance and knowledge by description and introduces important theories of Plato, Aristotle, René Descartes, David Hume, John Locke, Immanuel Kant, Georg Wilhelm Friedrich Hegel and others to lay the foundation for philosophical inquiry by general readers and scholars alike. "In the following pages I have confined myself in the main to those problems of philosophy in regard to which I thought it possible to say something positive and constructive, since merely negative criticism seemed out of place. For this reason, theory of knowledge occupies a larger space than metaphysics in the present volume, and some topics much discussed by philosophers are treated very briefly, if at all. (shrink)

In ”Formal Problems about Knowledge,” Roy Sorensen examines epistemological issues that have logical aspects. He uses Fitch's proof for unknowables and the surprise test paradox to illustrate the hopes of the modal logicians who developed epistemic logic, and he considers the epistemology of proof with the help of the knower paradox. One solution to this paradox is that knowledge is not closed under deduction. Sorensen reviews the broader history of this maneuver along with the relevant alternatives model of knowledge which (...) assumes that ”know” is an absolute term like ”flat.” Sorensen argues that the difference between epistemic absolute terms and extensional absolute terms gives rise to an asymmetry that undermines recent claims that there is a structural parallel between the supervaluational and epistemicist theories of vagueness, and he suggests that we have overestimated the ability of logical demonstration to produce knowledge. (shrink)

The paper discusses one of the central problems of contemporary formal semantics — counterexamples to the predictions of the theory of binding (due to N. Chomsky). In particular, the author addresses cases of the so-called coreferential readings of reflexive pronouns which are standardly predicted to receive only the bound reading. The author examines theories of T. Reinhart and I. Heim and suggests an extension ofthe latter theory in order to enable it to account for the aforementioned readings of reflexive pronouns.

The Problem of Perception is a pervasive and traditional problem about our ordinary conception of perceptual experience. The problem is created by the phenomena of perceptual illusion and hallucination: if these kinds of error are possible, how can perceptual experience be what we ordinarily understand it to be: something that enables direct perception of the world? These possibilities of error challenge the intelligibility of our ordinary conception of perceptual experience; the major theories of experience are responses to (...) this challenge. (shrink)

Immensely intelligible, thought-provoking guide by Nobel prize-winner considers such topics as the distinction between appearance and reality, the existence and nature of matter, idealism, inductive logic, intuitive knowledge, many other subjects. For students and general readers, there is no finer introduction to philosophy than this informative, affordable and highly readable edition that is "concise, free from technical terms, and perfectly clear to the general reader with no prior knowledge of the subject."—The Booklist of the American Library Association.

The author gives a critical and comprehensive study of the fundamental problem of universals in Indian Philosophy. The centre of the study is the controversy between the Nyaya-Vaisesika and the Mimamsa realists on the one hand and the Buddhist nominalists on the other. The author discusses not only the epistemological and metaphysical approach to the problem of universals but also the semantic approach made by the various systems of Indian Philosophy. In this context the view of the Grammarions (...) with special reference to Bhartrhari has been discussed in some detail. A brief but critical analysis of some of the main trends of thought on universals in Western Philosophy--beginning from Pluto to the contemporary philosophers--has also been given. Besides his scholarly and eminently readable treatment of fundamental problem of universals, the author has attempted to give his own solution of the problem. It is based on the recurrent identities and similarities which are the principles of grouping and which form the foundation of our thought and speech. (shrink)

The problem of imaginative resistance holds interest for aestheticians, literary theorists, ethicists, philosophers of mind, and epistemologists. We present a somewhat opinionated overview of the philosophical discussion to date. We begin by introducing the phenomenon of imaginative resistance. We then review existing responses to the problem, giving special attention to recent research directions. Finally, we consider the philosophical significance that imaginative resistance has—or, at least, is alleged to have—for issues in moral psychology, theories of cognitive architecture, and modal (...) epistemology. (shrink)